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).

7 files changed, 104 insertions, 98 deletions

diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v
index f35e2c1cc..e71b24018 100644
--- a/src/Algebra/Field.v
+++ b/src/Algebra/Field.v
@@ -12,12 +12,12 @@ Section Field.
   Local Infix "+" := add. Local Infix "*" := mul.
 
   Lemma right_multiplicative_inverse : forall x : T, ~ eq x zero -> eq (mul x (inv x)) one.
-  Proof.
+  Proof using Type*.
     intros. rewrite commutative. auto using left_multiplicative_inverse.
   Qed.
 
   Lemma left_inv_unique x ix : ix * x = one -> ix = inv x.
-  Proof.
+  Proof using Type*.
     intro Hix.
     assert (ix*x*inv x = inv x).
     - rewrite Hix, left_identity; reflexivity.
@@ -28,17 +28,17 @@ Section Field.
   Definition inv_unique := left_inv_unique.
 
   Lemma right_inv_unique x ix : x * ix = one -> ix = inv x.
-  Proof. rewrite commutative. apply left_inv_unique. Qed.
+  Proof using Type*. rewrite commutative. apply left_inv_unique. Qed.
 
   Lemma div_one x : div x one = x.
-  Proof.
+  Proof using Type*.
     rewrite field_div_definition.
     rewrite <-(inv_unique 1 1); apply monoid_is_right_identity.
   Qed.
 
   Lemma mul_cancel_l_iff : forall x y, y <> 0 ->
                                        (x * y = y <-> x = one).
-  Proof.
+  Proof using Type*.
     intros.
     split; intros.
     + rewrite <-(right_multiplicative_inverse y) by assumption.
@@ -50,7 +50,7 @@ Section Field.
   Qed.
 
   Lemma field_theory_for_stdlib_tactic : Field_theory.field_theory 0 1 add mul sub opp div inv eq.
-  Proof.
+  Proof using Type*.
     constructor.
     { apply Ring.ring_theory_for_stdlib_tactic. }
     { intro H01. symmetry in H01. auto using (zero_neq_one(eq:=eq)). }
@@ -61,7 +61,7 @@ Section Field.
   Context {eq_dec:DecidableRel eq}.
 
   Global Instance is_mul_nonzero_nonzero : @is_zero_product_zero_factor T eq 0 mul.
-  Proof.
+  Proof using Type*.
     split. intros x y Hxy.
     eapply not_not; try typeclasses eauto; []; intuition idtac; eapply (zero_neq_one(eq:=eq)).
     transitivity ((inv y * (inv x * x)) * y).
@@ -71,7 +71,7 @@ Section Field.
   Qed.
 
   Global Instance integral_domain : @integral_domain T eq zero one opp add sub mul.
-  Proof.
+  Proof using Type*.
     split; auto using field_commutative_ring, field_is_zero_neq_one, is_mul_nonzero_nonzero.
   Qed.
 End Field.
@@ -126,7 +126,7 @@ Section Homomorphism.
   Lemma homomorphism_multiplicative_inverse
     : forall x, not (EQ x ZERO)
                 -> phi (INV x) = inv (phi x).
-  Proof.
+  Proof using Type*.
     intros.
     eapply inv_unique.
     rewrite <-Ring.homomorphism_mul.
@@ -137,14 +137,14 @@ Section Homomorphism.
         { EQ_dec : DecidableRel EQ }
     : forall x, (EQ x ZERO -> phi (INV x) = inv (phi x))
                 -> phi (INV x) = inv (phi x).
-  Proof.
+  Proof using Type*.
     intros x ?; destruct (dec (EQ x ZERO)); auto using homomorphism_multiplicative_inverse.
   Qed.
 
   Lemma homomorphism_div
     : forall x y, not (EQ y ZERO)
                   -> phi (DIV x y) = div (phi x) (phi y).
-  Proof.
+  Proof using Type*.
     intros. rewrite !field_div_definition.
     rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse;
       (eauto || reflexivity).
@@ -154,7 +154,7 @@ Section Homomorphism.
         { EQ_dec : DecidableRel EQ }
     : forall x y, (EQ y ZERO -> phi (INV y) = inv (phi y))
                   -> phi (DIV x y) = div (phi x) (phi y).
-  Proof.
+  Proof using Type*.
     intros. rewrite !field_div_definition.
     rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse_complete;
       (eauto || reflexivity).
@@ -181,7 +181,7 @@ Section Homomorphism_rev.
     : @field H eq zero one opp add sub mul inv div
       /\ @Ring.is_homomorphism F EQ ONE ADD MUL H eq one add mul phi
       /\ @Ring.is_homomorphism H eq one add mul F EQ ONE ADD MUL phi'.
-  Proof.
+  Proof using Type*.
     repeat match goal with
            | [ H : field |- _ ] => destruct H; try clear H
            | [ H : commutative_ring |- _ ] => destruct H; try clear H
@@ -320,7 +320,7 @@ Section FieldSquareRoot.
   Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
   Local Infix "+" := add. Local Infix "*" := mul.
   Lemma only_two_square_roots_choice x y z : x * x = z -> y * y = z -> x = y \/ x = opp y.
-  Proof.
+  Proof using Type*.
     intros.
     setoid_rewrite <-sub_zero_iff.
     eapply zero_product_zero_factor.
diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v
index 2df673163..0743729c2 100644
--- a/src/Algebra/Field_test.v
+++ b/src/Algebra/Field_test.v
@@ -13,33 +13,37 @@ Module _fsatz_test.
     Local Infix "-" := sub. Local Infix "/" := div.
 
     Lemma inv_hyp a b c d (H:a*inv b=inv d*c) (bnz:b<>0) (dnz:d<>0) : a*d = b*c.
-    Proof. fsatz. Qed.
+    Proof using Type*. fsatz. Qed.
 
     Lemma inv_goal a b c d (H:a=b+c) (anz:a<>0) : inv a*d + 1 = (d+b+c)*inv(b+c).
-    Proof. fsatz. Qed.
+    Proof using Type*. fsatz. Qed.
 
     Lemma div_hyp a b c d (H:a/b=c/d) (bnz:b<>0) (dnz:d<>0) : a*d = b*c.
-    Proof. fsatz. Qed.
+    Proof using Type*. fsatz. Qed.
 
     Lemma div_goal a b c d (H:a=b+c) (anz:a<>0) : d/a + 1 = (d+b+c)/(b+c).
-    Proof. fsatz. Qed.
+    Proof using Type*. fsatz. Qed.
 
     Lemma zero_neq_one : 0 <> 1.
-    Proof. fsatz. Qed.
+    Proof using Type*. fsatz. Qed.
 
     Lemma only_two_square_roots x y : x * x = y * y -> x <> opp y -> x = y.
-    Proof. intros; fsatz. Qed.
+    Proof using Type*. intros; fsatz. Qed.
 
     Lemma transitivity_contradiction a b c (ab:a=b) (bc:b=c) (X:a<>c) : False.
-    Proof. fsatz. Qed.
+    Proof using Type*. fsatz. Qed.
 
     Lemma algebraic_contradiction a b c (A:a+b=c) (B:a-b=c) (X:a*a - b*b <> c*c) : False.
-    Proof. fsatz. Qed.
+    Proof using Type*. fsatz. Qed.
 
     Lemma division_by_zero_in_hyps (bad:1/0 + 1 = (1+1)/0): 1 = 1.
-    Proof. fsatz. Qed.
-    Lemma division_by_zero_in_hyps_eq_neq (bad:1/0 + 1 = (1+1)/0): 1 <> 0. fsatz. Qed.
-    Lemma division_by_zero_in_hyps_neq_neq (bad:1/0 <> (1+1)/0): 1 <> 0. fsatz. Qed.
+    Proof using Type*. fsatz. Qed.
+    Lemma division_by_zero_in_hyps_eq_neq (bad:1/0 + 1 = (1+1)/0): 1 <> 0.
+    Proof using Type*.
+ fsatz. Qed.
+    Lemma division_by_zero_in_hyps_neq_neq (bad:1/0 <> (1+1)/0): 1 <> 0.
+    Proof using Type*.
+ fsatz. Qed.
     Import BinNums.
 
     Context {char_ge_16:@Ring.char_ge F eq zero one opp add sub mul 16}.
@@ -50,10 +54,10 @@ Module _fsatz_test.
     Local Notation nine := (three+three+three) (only parsing).
 
     Lemma fractional_equation_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = three/(x+two) + seven*inv(x-1)) : x = opp one / (three+two).
-    Proof. fsatz. Qed.
+    Proof using Type*. fsatz. Qed.
 
     Lemma fractional_equation_no_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = opp three/(x+two) + seven*inv(x-1)) : False.
-    Proof. fsatz. Qed.
+    Proof using Type*. fsatz. Qed.
 
     Local Notation "x ^ 2" := (x*x).
     Lemma recursive_nonzero_solving
@@ -62,7 +66,7 @@ Module _fsatz_test.
           (Hsqrt : sqrt_a^2 = a)
           (Hfrac : (sqrt_a / y)^2 <> d)
       : x^2 = (y^2 - one) / (d * y^2 - a).
-    Proof. fsatz. Qed.
+    Proof using eq_dec fld. fsatz. Qed.
 
     Local Notation "x ^ 3" := (x^2*x).
     Lemma weierstrass_associativity_main a b x1 y1 x2 y2 x4 y4
@@ -86,6 +90,6 @@ Module _fsatz_test.
           x9 (Hx9: x9 = λ9^2-x1-x6)
           y9 (Hy9: y9 = λ9*(x1-x9)-y1)
       : x7 = x9 /\ y7 = y9.
-    Proof. fsatz_prepare_hyps; split; fsatz. Qed.
+    Proof using Type*. fsatz_prepare_hyps; split; fsatz. Qed.
   End _test.
 End _fsatz_test.
\ No newline at end of file
diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v
index b053fc844..64e378281 100644
--- a/src/Algebra/Group.v
+++ b/src/Algebra/Group.v
@@ -9,16 +9,16 @@ Section BasicProperties.
   Local Open Scope eq_scope.
 
   Lemma cancel_left : forall z x y, z*x = z*y <-> x = y.
-  Proof. eauto using Monoid.cancel_left, left_inverse. Qed.
+  Proof using Type*. eauto using Monoid.cancel_left, left_inverse. Qed.
   Lemma cancel_right : forall z x y, x*z = y*z <-> x = y.
-  Proof. eauto using Monoid.cancel_right, right_inverse. Qed.
+  Proof using Type*. eauto using Monoid.cancel_right, right_inverse. Qed.
   Lemma inv_inv x : inv(inv(x)) = x.
-  Proof. eauto using Monoid.inv_inv, left_inverse. Qed.
+  Proof using Type*. eauto using Monoid.inv_inv, left_inverse. Qed.
   Lemma inv_op_ext x y : (inv y*inv x)*(x*y) =id.
-  Proof. eauto using Monoid.inv_op, left_inverse. Qed.
+  Proof using Type*. eauto using Monoid.inv_op, left_inverse. Qed.
 
   Lemma inv_unique x ix : ix * x = id -> ix = inv x.
-  Proof.
+  Proof using Type*.
     intro Hix.
     cut (ix*x*inv x = inv x).
     - rewrite <-associative, right_inverse, right_identity; trivial.
@@ -26,14 +26,14 @@ Section BasicProperties.
   Qed.
 
   Lemma inv_bijective x y : inv x = inv y <-> x = y.
-  Proof.
+  Proof using Type*.
     split; intro Hi; rewrite ?Hi; try reflexivity.
     assert (Hii:inv (inv x) = inv (inv y)) by (rewrite Hi; reflexivity).
     rewrite 2inv_inv in Hii; exact Hii.
   Qed.
 
   Lemma inv_op x y : inv (x*y) = inv y*inv x.
-  Proof.
+  Proof using Type*.
     symmetry. etransitivity.
     2:eapply inv_unique.
     2:eapply inv_op_ext.
@@ -41,19 +41,19 @@ Section BasicProperties.
   Qed.
 
   Lemma inv_id : inv id = id.
-  Proof. symmetry. eapply inv_unique, left_identity. Qed.
+  Proof using Type*. symmetry. eapply inv_unique, left_identity. Qed.
 
   Lemma inv_id_iff x : inv x = id <-> x = id.
-  Proof.
+  Proof using Type*.
     split; intro Hi; rewrite ?Hi, ?inv_id; try reflexivity.
     rewrite <-inv_id, inv_bijective in Hi; exact Hi.
   Qed.
 
   Lemma inv_nonzero_nonzero x : x <> id <-> inv x <> id.
-  Proof. setoid_rewrite inv_id_iff; reflexivity. Qed.
+  Proof using Type*. setoid_rewrite inv_id_iff; reflexivity. Qed.
 
   Lemma eq_r_opp_r_inv a b c : a = op c (inv b) <-> op a b = c.
-  Proof.
+  Proof using Type*.
     split; intro Hx; rewrite Hx || rewrite <-Hx;
       rewrite <-!associative, ?left_inverse, ?right_inverse, right_identity;
       reflexivity.
@@ -62,9 +62,9 @@ Section BasicProperties.
   Section ZeroNeqOne.
     Context {one} `{is_zero_neq_one T eq id one}.
     Lemma opp_one_neq_zero : inv one <> id.
-    Proof. setoid_rewrite inv_id_iff. exact one_neq_zero. Qed.
+    Proof using Type*. setoid_rewrite inv_id_iff. exact one_neq_zero. Qed.
     Lemma zero_neq_opp_one : id <> inv one.
-    Proof. intro Hx. symmetry in Hx. eauto using opp_one_neq_zero. Qed.
+    Proof using Type*. intro Hx. symmetry in Hx. eauto using opp_one_neq_zero. Qed.
   End ZeroNeqOne.
 End BasicProperties.
 
@@ -75,14 +75,14 @@ Section Homomorphism.
   Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
 
   Lemma homomorphism_id : phi ID = id.
-  Proof.
+  Proof using Type*.
     assert (Hii: op (phi ID) (phi ID) = op (phi ID) id) by
         (rewrite <- Monoid.homomorphism, left_identity, right_identity; reflexivity).
     rewrite cancel_left in Hii; exact Hii.
   Qed.
 
   Lemma homomorphism_inv x : phi (INV x) = inv (phi x).
-  Proof.
+  Proof using Type*.
     apply inv_unique.
     rewrite <- Monoid.homomorphism, left_inverse, homomorphism_id; reflexivity.
   Qed.
@@ -91,11 +91,11 @@ Section Homomorphism.
     Context {MUL} {MUL_is_scalarmult:@ScalarMult.is_scalarmult G EQ OP ID MUL }.
     Context {mul} {mul_is_scalarmult:@ScalarMult.is_scalarmult H eq op id mul }.
     Lemma homomorphism_scalarmult n P : phi (MUL n P) = mul n (phi P).
-    Proof. eapply ScalarMult.homomorphism_scalarmult, homomorphism_id. Qed.
+    Proof using Type*. eapply ScalarMult.homomorphism_scalarmult, homomorphism_id. Qed.
 
     Import ScalarMult.
     Lemma opp_mul : forall n P, inv (mul n P) = mul n (inv P).
-    Proof.
+    Proof using groupH mul_is_scalarmult.
       induction n; intros.
       { rewrite !scalarmult_0_l, inv_id; reflexivity. }
       { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1.
@@ -117,7 +117,7 @@ Section Homomorphism_rev.
 
   Lemma group_from_redundant_representation
     : @group H eq op id inv /\ @Monoid.is_homomorphism G EQ OP H eq op phi /\ @Monoid.is_homomorphism H eq op G EQ OP phi'.
-  Proof.
+  Proof using Type*.
     repeat match goal with
            | [ H : _/\_ |- _ ] => destruct H; try clear H
            | [ H : group |- _ ] => destruct H; try clear H
@@ -141,7 +141,7 @@ Section Homomorphism_rev.
 
   Definition homomorphism_from_redundant_representation
     : @Monoid.is_homomorphism G EQ OP H eq op phi.
-  Proof.
+  Proof using groupG phi'_eq phi'_op phi'_phi_id.
     split; repeat intro; apply phi'_eq; rewrite ?phi'_op, ?phi'_phi_id; easy.
   Qed.
 End Homomorphism_rev.
@@ -204,7 +204,7 @@ Section HomomorphismComposition.
         {phi'':G->K}
         (Hphi'' : forall x, eqK (phi' (phi x)) (phi'' x))
     : @Monoid.is_homomorphism G EQ OP K eqK opK phi''.
-  Proof.
+  Proof using Hphi Hphi' groupK.
     split; repeat intro; rewrite <- !Hphi''.
     { rewrite !Monoid.homomorphism; reflexivity. }
     { apply Hphi', Hphi; assumption. }
diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v
index 083c10242..4ab50c6e3 100644
--- a/src/Algebra/IntegralDomain.v
+++ b/src/Algebra/IntegralDomain.v
@@ -11,12 +11,12 @@ Module IntegralDomain.
 
     Lemma nonzero_product_iff_nonzero_factors :
       forall x y : T, ~ eq (mul x y) zero <-> ~ eq x zero /\ ~ eq y zero.
-    Proof. setoid_rewrite Ring.zero_product_iff_zero_factor; intuition. Qed.
+    Proof using Type*. setoid_rewrite Ring.zero_product_iff_zero_factor; intuition. Qed.
 
     Global Instance Integral_domain :
       @Integral_domain.Integral_domain T zero one add mul sub opp eq Ring.Ncring_Ring_ops
                                        Ring.Ncring_Ring Ring.Cring_Cring_commutative_ring.
-    Proof. split; cbv; eauto using zero_product_zero_factor, one_neq_zero. Qed.
+    Proof using Type. split; cbv; eauto using zero_product_zero_factor, one_neq_zero. Qed.
   End IntegralDomain.
 
   Module _LargeCharacteristicReflective.
@@ -51,14 +51,14 @@ Module IntegralDomain.
       Let of_Z := (@Ring.of_Z R zero one opp add).
 
       Lemma CtoZ_correct c : of_Z (CtoZ c) = denote c.
-      Proof.
+      Proof using ring.
         induction c; simpl CtoZ; simpl denote;
           repeat (rewrite_hyp ?* || Ring.push_homomorphism of_Z); reflexivity.
       Qed.
 
       (* TODO: move *)
       Lemma nonzero_of_Z_abs z : of_Z (Z.abs z) <> zero <-> of_Z z <> zero.
-      Proof.
+      Proof using ring.
         destruct z; simpl Z.abs; [reflexivity..|].
         simpl of_Z. setoid_rewrite opp_zero_iff. reflexivity.
       Qed.
@@ -70,13 +70,13 @@ Module IntegralDomain.
           match n with N0 => false | N.pos p => BinPos.Pos.ltb p C end.
         Lemma is_factor_nonzero_correct (n:N) (refl:Logic.eq (is_factor_nonzero n) true)
           : of_Z (Z.of_N n) <> zero.
-        Proof.
+        Proof using char_ge_C.
           destruct n; [discriminate|]; rewrite Znat.positive_N_Z; apply char_ge_C, Pos.ltb_lt, refl.
         Qed.
 
         Lemma RZN_product_nonzero l (H : forall x : N, List.In x l -> of_Z (Z.of_N x) <> zero)
           : of_Z (Z.of_N (List.fold_right N.mul 1%N l)) <> zero.
-        Proof.
+        Proof using HC char_ge_C ring zpzf.
           rewrite <-List.Forall_forall in H; induction H; simpl List.fold_right.
           { eapply char_ge_C; assumption. }
           { rewrite Znat.N2Z.inj_mul; Ring.push_homomorphism of_Z.
@@ -90,7 +90,7 @@ Module IntegralDomain.
           end.
         Lemma is_constant_nonzero_correct z (refl:Logic.eq (is_constant_nonzero z) true)
           : of_Z z <> zero.
-        Proof.
+        Proof using HC char_ge_C ring zpzf.
             rewrite <-nonzero_of_Z_abs, <-Znat.N2Z.inj_abs_N.
             repeat match goal with
                    | _ => progress cbv [is_constant_nonzero] in *
@@ -109,7 +109,7 @@ Module IntegralDomain.
           | _ => is_constant_nonzero (CtoZ c)
           end.
         Lemma is_nonzero_correct' c (refl:Logic.eq (is_nonzero c) true) : denote c <> zero.
-        Proof.
+        Proof using HC char_ge_C ring zpzf.
           induction c;
             repeat match goal with
                    | H:_|-_ => progress rewrite Bool.andb_true_iff in H; destruct H
@@ -131,7 +131,7 @@ Module IntegralDomain.
             (char_ge_C:@Ring.char_ge R eq zero one opp add sub mul C)
             c (refl:Logic.eq (andb (Pos.ltb xH C) (is_nonzero C c)) true)
         : denote c <> zero.
-      Proof.
+      Proof using ring zpzf.
         rewrite Bool.andb_true_iff in refl; destruct refl.
         eapply @is_nonzero_correct'; try apply Pos.ltb_lt; eauto.
       Qed.
diff --git a/src/Algebra/Monoid.v b/src/Algebra/Monoid.v
index 565058cf7..bd15290c7 100644
--- a/src/Algebra/Monoid.v
+++ b/src/Algebra/Monoid.v
@@ -11,7 +11,7 @@ Section Monoid.
 
   Lemma cancel_right z iz (Hinv:op z iz = id) :
     forall x y, x * z = y * z <-> x = y.
-  Proof.
+  Proof using Type*.
     split; intros.
     { assert (op (op x z) iz = op (op y z) iz) as Hcut by (rewrite_hyp ->!*; reflexivity).
       rewrite <-associative in Hcut.
@@ -21,7 +21,7 @@ Section Monoid.
 
   Lemma cancel_left z iz (Hinv:op iz z = id) :
     forall x y, z * x = z * y <-> x = y.
-  Proof.
+  Proof using Type*.
     split; intros.
     { assert (op iz (op z x) = op iz (op z y)) as Hcut by (rewrite_hyp ->!*; reflexivity).
       rewrite !associative, !Hinv, !left_identity in Hcut; exact Hcut. }
@@ -29,14 +29,14 @@ Section Monoid.
   Qed.
 
   Lemma inv_inv x ix iix : ix*x = id -> iix*ix = id -> iix = x.
-  Proof.
+  Proof using Type*.
     intros Hi Hii.
     assert (H:op iix id = op iix (op ix x)) by (rewrite Hi; reflexivity).
     rewrite associative, Hii, left_identity, right_identity in H; exact H.
   Qed.
 
   Lemma inv_op x y ix iy : ix*x = id -> iy*y = id -> (iy*ix)*(x*y) =id.
-  Proof.
+  Proof using Type*.
     intros Hx Hy.
     cut (iy * (ix*x) * y = id); try intro H.
     { rewrite <-!associative; rewrite <-!associative in H; exact H. }
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v
index 2b0e1ba80..cff27bdb3 100644
--- a/src/Algebra/Ring.v
+++ b/src/Algebra/Ring.v
@@ -15,7 +15,7 @@ Section Ring.
   Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul.
 
   Lemma mul_0_l : forall x, 0 * x = 0.
-  Proof.
+  Proof using Type*.
     intros.
     assert (0*x = 0*x) as Hx by reflexivity.
     rewrite <-(right_identity 0), right_distributive in Hx at 1.
@@ -24,7 +24,7 @@ Section Ring.
   Qed.
 
   Lemma mul_0_r : forall x, x * 0 = 0.
-  Proof.
+  Proof using Type*.
     intros.
     assert (x*0 = x*0) as Hx by reflexivity.
     rewrite <-(left_identity 0), left_distributive in Hx at 1.
@@ -33,10 +33,10 @@ Section Ring.
   Qed.
 
   Lemma sub_0_l x : 0 - x = opp x.
-  Proof. rewrite ring_sub_definition. rewrite left_identity. reflexivity. Qed.
+  Proof using Type*. rewrite ring_sub_definition. rewrite left_identity. reflexivity. Qed.
 
   Lemma mul_opp_r x y : x * opp y = opp (x * y).
-  Proof.
+  Proof using Type*.
     assert (Ho:x*(opp y) + x*y = 0)
       by (rewrite <-left_distributive, left_inverse, mul_0_r; reflexivity).
     rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho.
@@ -44,7 +44,7 @@ Section Ring.
   Qed.
 
   Lemma mul_opp_l x y : opp x * y = opp (x * y).
-  Proof.
+  Proof using Type*.
     assert (Ho:opp x*y + x*y = 0)
       by (rewrite <-right_distributive, left_inverse, mul_0_l; reflexivity).
     rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho.
@@ -54,19 +54,19 @@ Section Ring.
   Definition opp_zero_iff : forall x, opp x = 0 <-> x = 0 := Group.inv_id_iff.
 
   Global Instance is_left_distributive_sub : is_left_distributive (eq:=eq)(add:=sub)(mul:=mul).
-  Proof.
+  Proof using Type*.
     split; intros. rewrite !ring_sub_definition, left_distributive.
     eapply Group.cancel_left, mul_opp_r.
   Qed.
 
   Global Instance is_right_distributive_sub : is_right_distributive (eq:=eq)(add:=sub)(mul:=mul).
-  Proof.
+  Proof using Type*.
     split; intros. rewrite !ring_sub_definition, right_distributive.
     eapply Group.cancel_left, mul_opp_l.
   Qed.
 
   Lemma sub_zero_iff x y : x - y = 0 <-> x = y.
-  Proof.
+  Proof using Type*.
     split; intro E.
     { rewrite <-(right_identity y), <- E, ring_sub_definition.
       rewrite commutative, <-associative, commutative.
@@ -75,25 +75,25 @@ Section Ring.
   Qed.
 
   Lemma neq_sub_neq_zero x y (Hxy:x<>y) : x-y <> 0.
-  Proof.
+  Proof using Type*.
     intro Hsub. apply Hxy. rewrite <-(left_identity y), <-Hsub, ring_sub_definition.
     rewrite <-associative, left_inverse, right_identity. reflexivity.
   Qed.
 
   Lemma zero_product_iff_zero_factor {Hzpzf:@is_zero_product_zero_factor T eq zero mul} :
     forall x y : T, eq (mul x y) zero <-> eq x zero \/ eq y zero.
-  Proof.
+  Proof using Type*.
     split; eauto using zero_product_zero_factor; [].
     intros [Hz|Hz]; rewrite Hz; eauto using mul_0_l, mul_0_r.
   Qed.
 
   Lemma nonzero_product_iff_nonzero_factor {Hzpzf:@is_zero_product_zero_factor T eq zero mul} :
     forall x y : T, not (eq (mul x y) zero) <-> (not (eq x zero) /\ not (eq y zero)).
-  Proof. intros; rewrite zero_product_iff_zero_factor; tauto. Qed.
+  Proof using Type*. intros; rewrite zero_product_iff_zero_factor; tauto. Qed.
 
   Global Instance Ncring_Ring_ops : @Ncring.Ring_ops T zero one add mul sub opp eq.
   Global Instance Ncring_Ring : @Ncring.Ring T zero one add mul sub opp eq Ncring_Ring_ops.
-  Proof.
+  Proof using Type*.
     split; exact _ || cbv; intros; eauto using left_identity, right_identity, commutative, associative, right_inverse, left_distributive, right_distributive, ring_sub_definition with core typeclass_instances.
     - (* TODO: why does [eauto using @left_identity with typeclass_instances] not work? *)
       eapply @left_identity; eauto with typeclass_instances.
@@ -121,23 +121,23 @@ Section Homomorphism.
   Context `{phi_homom:is_homomorphism}.
 
   Lemma homomorphism_zero : phi ZERO = zero.
-  Proof. apply Group.homomorphism_id. Qed.
+  Proof using Type*. apply Group.homomorphism_id. Qed.
 
   Lemma homomorphism_add : forall x y,  phi (ADD x y) = add (phi x) (phi y).
-  Proof. apply Monoid.homomorphism. Qed.
+  Proof using phi_homom. apply Monoid.homomorphism. Qed.
 
   Definition homomorphism_opp : forall x,  phi (OPP x) = opp (phi x) :=
     (Group.homomorphism_inv (INV:=OPP) (inv:=opp)).
 
   Lemma homomorphism_sub : forall x y, phi (SUB x y) = sub (phi x) (phi y).
-  Proof.
+  Proof using Type*.
     intros.
     rewrite !ring_sub_definition, Monoid.homomorphism, homomorphism_opp. reflexivity.
   Qed.
 
   Global Instance monoid_homomorphism_mul :
     Monoid.is_homomorphism (phi:=phi) (OP:=MUL) (op:=mul) (EQ:=EQ) (eq:=eq).
-  Proof. split; destruct phi_homom; assumption || exact _. Qed.
+  Proof using phi_homom. split; destruct phi_homom; assumption || exact _. Qed.
 End Homomorphism.
 
 (* TODO: file a Coq bug for rewrite_strat -- it should accept ltac variables *)
@@ -200,7 +200,7 @@ Section Isomorphism.
     : @ring H eq zero one opp add sub mul
       /\ @is_homomorphism F EQ ONE ADD MUL H eq one add mul phi
       /\ @is_homomorphism H eq one add mul F EQ ONE ADD MUL phi'.
-  Proof.
+  Proof using phi'_add phi'_eq phi'_mul phi'_one phi'_opp phi'_phi_id phi'_sub phi'_zero ringF.
     repeat match goal with
            | [ H : field |- _ ] => destruct H; try clear H
            | [ H : commutative_ring |- _ ] => destruct H; try clear H
@@ -236,10 +236,10 @@ Section TacticSupportCommutative.
 
   Global Instance Cring_Cring_commutative_ring :
     @Cring.Cring T zero one add mul sub opp eq Ncring_Ring_ops Ncring_Ring.
-  Proof. unfold Cring.Cring; intros; cbv. eapply commutative. Qed.
+  Proof using Type. unfold Cring.Cring; intros; cbv. eapply commutative. Qed.
 
   Lemma ring_theory_for_stdlib_tactic : Ring_theory.ring_theory zero one add mul sub opp eq.
-  Proof.
+  Proof using Type*.
     constructor; intros. (* TODO(automation): make [auto] do this? *)
     - apply left_identity.
     - apply commutative.
@@ -289,15 +289,15 @@ Section of_Z.
     end.
 
   Lemma of_Z_0 : of_Z 0 = Rzero.
-  Proof. reflexivity. Qed.
+  Proof using Type*. reflexivity. Qed.
 
   Lemma of_nat_add x :
     of_nat (Nat.add x 1) = Radd (of_nat x) Rone.
-  Proof. destruct x; rewrite ?Nat.add_1_r; reflexivity. Qed.
+  Proof using Type*. destruct x; rewrite ?Nat.add_1_r; reflexivity. Qed.
 
   Lemma of_nat_sub x (H: (0 < x)%nat):
     of_nat (Nat.sub x 1) = Rsub (of_nat x) Rone.
-  Proof.
+  Proof using Type*.
     induction x; [omega|simpl].
     rewrite <-of_nat_add.
     rewrite Nat.sub_0_r, Nat.add_1_r.
@@ -309,7 +309,7 @@ Section of_Z.
 
   Lemma of_Z_add_1_r :
     forall x, of_Z (Z.add x 1) = Radd (of_Z x) Rone.
-  Proof.
+  Proof using Type*.
     destruct x; [reflexivity| | ]; simpl of_Z.
     { rewrite Pos2Nat.inj_add, of_nat_add.
       reflexivity. }
@@ -330,7 +330,7 @@ Section of_Z.
 
   Lemma of_Z_sub_1_r :
     forall x, of_Z (Z.sub x 1) = Rsub (of_Z x) Rone.
-  Proof.
+  Proof using Type*.
     induction x.
     { simpl; rewrite ring_sub_definition, !left_identity;
         reflexivity. }
@@ -354,14 +354,14 @@ Section of_Z.
 
   Lemma of_Z_opp : forall a,
       of_Z (Z.opp a) = Ropp (of_Z a).
-  Proof.
+  Proof using Type*.
     destruct a; simpl; rewrite ?Group.inv_id, ?Group.inv_inv;
       reflexivity.
   Qed.
 
   Lemma of_Z_add : forall a b,
       of_Z (Z.add a b) = Radd (of_Z a) (of_Z b).
-  Proof.
+  Proof using Type*.
     intros.
     let x := match goal with |- ?x => x end in
     let f := match (eval pattern b in x) with ?f _ => f end in
@@ -381,7 +381,7 @@ Section of_Z.
 
   Lemma of_Z_mul : forall a b,
       of_Z (Z.mul a b) = Rmul (of_Z a) (of_Z b).
-  Proof.
+  Proof using Type*.
     intros.
     let x := match goal with |- ?x => x end in
     let f := match (eval pattern b in x) with ?f _ => f end in
@@ -408,7 +408,7 @@ Section of_Z.
       Z Logic.eq Z.one Z.add Z.mul
       R Req  Rone  Radd  Rmul
       of_Z.
-  Proof.
+  Proof using Type*.
     repeat constructor; intros.
     { apply of_Z_add. }
     { repeat intro; subst; reflexivity. }
diff --git a/src/Algebra/ScalarMult.v b/src/Algebra/ScalarMult.v
index 33c236775..5c17a6bb5 100644
--- a/src/Algebra/ScalarMult.v
+++ b/src/Algebra/ScalarMult.v
@@ -28,30 +28,32 @@ Section ScalarMultProperties.
     end.
 
   Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref.
-  Proof.
+  Proof using monoidG.
     repeat intro; subst.
     match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end.
     repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity.
   Qed.
 
   Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P.
+  Proof using Type*.
+
     induction n; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l).
   Qed.
 
   Lemma scalarmult_1_l : forall P, 1*P = P.
-  Proof. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed.
+  Proof using Type*. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed.
 
   Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P).
-  Proof.
+  Proof using Type*.
     induction n; intros;
       rewrite ?scalarmult_0_l, ?scalarmult_S_l, ?plus_Sn_m, ?plus_O_n, ?scalarmult_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity.
   Qed.
 
   Lemma scalarmult_zero_r : forall m, m * zero = zero.
-  Proof. induction m; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed.
+  Proof using Type*. induction m; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed.
 
   Lemma scalarmult_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P.
-  Proof.
+  Proof using Type*.
     induction n; intros.
     { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. }
     { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l.
@@ -59,10 +61,10 @@ Section ScalarMultProperties.
   Qed.
 
   Lemma scalarmult_times_order : forall l B, l*B = zero -> forall n, (l * n) * B = zero.
-  Proof. intros ? ? Hl ?. rewrite <-scalarmult_assoc, Hl, scalarmult_zero_r. reflexivity. Qed.
+  Proof using Type*. intros ? ? Hl ?. rewrite <-scalarmult_assoc, Hl, scalarmult_zero_r. reflexivity. Qed.
 
   Lemma scalarmult_mod_order : forall l B, l <> 0%nat -> l*B = zero -> forall n, n mod l * B = n * B.
-  Proof.
+  Proof using Type*.
     intros ? ? Hnz Hmod ?.
     rewrite (NPeano.Nat.div_mod n l Hnz) at 2.
     rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity.
@@ -79,7 +81,7 @@ Section ScalarMultHomomorphism.
   Context (phi_ZERO:phi ZERO = zero).
 
   Lemma homomorphism_scalarmult : forall n P, phi (MUL n P) = mul n (phi P).
-  Proof.
+  Proof using Type*.
     setoid_rewrite scalarmult_ext.
     induction n; intros; simpl; rewrite ?Monoid.homomorphism, ?IHn; easy.
   Qed.