Add [Proof using] to most proofs

This closes #146 and makes `make quick` faster.

The changes were generated by adding [Global Set Suggest Proof Using.]
to GlobalSettings.v, and then following [the instructions for a script I
wrote](https://github.com/JasonGross/coq-tools#proof-using-helper).

1 files changed, 4 insertions, 4 deletions

diff --git a/src/Reflection/SmartCastWf.v b/src/Reflection/SmartCastWf.v
index ef5d0170d..4c5601669 100644
--- a/src/Reflection/SmartCastWf.v
+++ b/src/Reflection/SmartCastWf.v
@@ -27,7 +27,7 @@ Section language.
   Lemma wff_SmartCast_base {var1 var2 A A'} G e1 e2
         (Hwf : wff (var1:=var1) (var2:=var2) G (t:=Tbase A) e1 e2)
     : wff G (t:=Tbase A') (SmartCast_base e1) (SmartCast_base e2).
-  Proof.
+  Proof using wff_Cast.
     unfold SmartCast_base; destruct (Sumbool.sumbool_of_bool (base_type_beq A A')) as [H|H].
     { destruct (base_type_bl_transparent A A' H); assumption. }
     { auto. }
@@ -44,7 +44,7 @@ Section language.
       | None, None => True
       | Some _, None | None, Some _ => False
       end.
-  Proof.
+  Proof using wff_Cast.
     break_innermost_match; revert dependent B; induction A, B;
       repeat match goal with
              | _ => progress simpl in *
@@ -67,7 +67,7 @@ Section language.
     : SmartCast A B = Some f1 -> SmartCast A B = Some f2
       -> forall e1 e2,
           wff (var1:=var1) (var2:=var2) (flatten_binding_list e1 e2) (f1 e1) (f2 e2).
-  Proof.
+  Proof using wff_Cast.
     intros H1 H2; generalize (@wff_SmartCast_match var1 var2 A B).
     rewrite H1, H2; trivial.
   Qed.
@@ -76,7 +76,7 @@ Section language.
     : SmartCast A B = Some f1 -> SmartCast A B = Some f2
       -> forall e1 e2,
           wff (var1:=var1) (var2:=var2) (flatten_binding_list e1 e2 ++ G) (f1 e1) (f2 e2).
-  Proof.
+  Proof using wff_Cast.
     intros; eapply wff_in_impl_Proper; [ eapply wff_SmartCast; eassumption | auto ].
   Qed.
 End language.