Patch to partially address issue #756

Author: andrew-appel

floyd/for_lemmas.v

@@ -824,13 +824,16 @@ intros. eapply derives_trans; try eassumption; auto.
 Qed.
 
 Ltac quick_typecheck3 :=
+ (* do not clear hyps anymore!  See issue #772 
  clear;
  repeat match goal with
  | H := _ |- _ => clear H
  | H : _ |- _ => clear H
- end;
+ end; *)
  apply quick_derives_right; clear; go_lowerx; intros;
- clear; repeat apply andp_right; auto; fail.
+ clear; repeat apply andp_right; 
+ try apply derives_refl;  (* see issue #756 *)
+ auto; fail.
 
 Ltac default_entailer_for_load_store :=
   repeat match goal with H := _ |- _ => clear H end;

floyd/sc_set_load_store.v

@@ -1785,7 +1785,9 @@ Qed.
 Ltac quick_typecheck3 :=
   (* do not clear hyps anymore!  See issue #772 *)
  apply quick_derives_right; go_lowerx; intros;
- repeat apply andp_right; auto; fail.
+ repeat apply andp_right; 
+ try apply derives_refl;  (* see issue #756 *)
+ auto; fail.
 
 Ltac default_entailer_for_load_store :=
   (* Don't clear!  See issue #772 repeat match goal with H := _ |- _ => clear H end; *)