Improvements in deadvars

[andrew-appel]

These two fixes should be made in floyd/deadvars.v

1. Ltac inhabited_value should unfold only AFTER checking above the line. Even the fix shown is not quite perfect. It's better than before, in that if any value of the unfolded type exists above the line then it will succeed instead of fail. But if no value of the unfolded type is above the line, then the error message will be for the unfolded type rather than the original.

Ltac inhabited_value T ::=
 match T with
 | nat => constr:(O)
 | Z => constr:(0%Z)
 | list ?A => constr:(@nil A)
 | positive => xH
 | bool => false
 | prod ?A ?B => let x := inhabited_value A in
                           let y := inhabited_value B in
                               constr:(pair x y)
 (* delete the old "eval unfold" that was here, and put it below as shown: *)
 | _ => match goal with
            | x:T |- _ => x 
            | x := _ : T |- _ => x
            | _ => let t := eval unfold T in T in
                   tryif constr_eq t T 
                   then fail 3 "cannot prove that type" T "is inhabited, so cannot compute deadvars.  Fix this by asserting (X:"T") above the line"
                   else inhabited_value t
            end
 end.

2. Ltac deadvars should not mask the failure of find_dead_vars with a different fail 99.

Ltac deadvars := 
 lazymatch goal with
 | X := @abbreviate ret_assert ?Q |-
    semax _ ?P ?c ?Y =>
    check_POSTCONDITION;
    tryif constr_eq X Y then idtac else fail 99 "@abbreviate ret_assert above the line does not match postcondition";
    match find_dead_vars P c Q with
    | nil => idtac
    | ?d =>  idtac "Dropping dead vars!"; drop_LOCALs d
     end  (* remove the fail 99 from here, and put it above as shown *)
 | |- semax _ _ _ _ => 
       check_POSTCONDITION;
       fail "deadvars: Postcondition must be an abbreviated local definition (POSTCONDITION); try abbreviate_semax first"
 | |- _ |-- _ => idtac
 | |- _ => fail "deadvars: the proof goal should be a semax"
 end.