Don't rely on autogenerated names

This fixes all of the private-names warnings emitted by
compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus
the ones in coqprime, which I didn't touch).

4 files changed, 29 insertions, 21 deletions

diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v
index b5b65f161..d46f10190 100644
--- a/src/Algebra/Field.v
+++ b/src/Algebra/Field.v
@@ -19,7 +19,7 @@ Section Field.
   Lemma left_inv_unique x ix : ix * x = one -> ix = inv x.
   Proof using Type*.
     intro Hix.
-    assert (ix*x*inv x = inv x).
+    assert (H0 : ix*x*inv x = inv x).
     - rewrite Hix, left_identity; reflexivity.
     - rewrite <-associative, right_multiplicative_inverse, right_identity in H0; trivial.
       intro eq_x_0. rewrite eq_x_0, Ring.mul_0_r in Hix.
@@ -39,8 +39,8 @@ Section Field.
   Lemma mul_cancel_l_iff : forall x y, y <> 0 ->
                                        (x * y = y <-> x = one).
   Proof using Type*.
-    intros.
-    split; intros.
+    intros x y H0.
+    split; intros H1.
     + rewrite <-(right_multiplicative_inverse y) by assumption.
       rewrite <-H1 at 1; rewrite <-associative.
       rewrite right_multiplicative_inverse by assumption.
diff --git a/src/Algebra/Monoid.v b/src/Algebra/Monoid.v
index e5755b6f0..aa30865c3 100644
--- a/src/Algebra/Monoid.v
+++ b/src/Algebra/Monoid.v
@@ -12,7 +12,7 @@ Section Monoid.
   Lemma cancel_right z iz (Hinv:op z iz = id) :
     forall x y, x * z = y * z <-> x = y.
   Proof using Type*.
-    split; intros.
+    intros x y; split; intro.
     { assert (op (op x z) iz = op (op y z) iz) as Hcut by (rewrite_hyp ->!*; reflexivity).
       rewrite <-associative in Hcut.
       rewrite <-!associative, !Hinv, !right_identity in Hcut; exact Hcut. }
@@ -22,7 +22,7 @@ Section Monoid.
   Lemma cancel_left z iz (Hinv:op iz z = id) :
     forall x y, z * x = z * y <-> x = y.
   Proof using Type*.
-    split; intros.
+    intros x y; 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. }
     { rewrite_hyp ->!*; reflexivity. }
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v
index 2e3bcba58..bf45155c8 100644
--- a/src/Algebra/Ring.v
+++ b/src/Algebra/Ring.v
@@ -4,6 +4,7 @@ Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.OnSubterms.
 Require Import Crypto.Util.Tactics.Revert.
+Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Group Crypto.Algebra.Monoid.
 Require Coq.ZArith.ZArith Coq.PArith.PArith.
 
@@ -16,7 +17,7 @@ Section Ring.
 
   Lemma mul_0_l : forall x, 0 * x = 0.
   Proof using Type*.
-    intros.
+    intros x.
     assert (0*x = 0*x) as Hx by reflexivity.
     rewrite <-(right_identity 0), right_distributive in Hx at 1.
     assert (0*x + 0*x - 0*x = 0*x - 0*x) as Hxx by (rewrite Hx; reflexivity).
@@ -25,7 +26,7 @@ Section Ring.
 
   Lemma mul_0_r : forall x, x * 0 = 0.
   Proof using Type*.
-    intros.
+    intros x.
     assert (x*0 = x*0) as Hx by reflexivity.
     rewrite <-(left_identity 0), left_distributive in Hx at 1.
     assert (opp (x*0) + (x*0 + x*0)  = opp (x*0) + x*0) as Hxx by (rewrite Hx; reflexivity).
@@ -331,7 +332,7 @@ Section of_Z.
   Lemma of_Z_sub_1_r :
     forall x, of_Z (Z.sub x 1) = Rsub (of_Z x) Rone.
   Proof using Type*.
-    induction x.
+    induction x as [|p|].
     { simpl; rewrite ring_sub_definition, !left_identity;
         reflexivity. }
     { case_eq (1 ?= p)%positive; intros;
@@ -362,19 +363,27 @@ Section of_Z.
   Lemma of_Z_add : forall a b,
       of_Z (Z.add a b) = Radd (of_Z a) (of_Z b).
   Proof using Type*.
-    intros.
+    intros a b.
     let x := match goal with |- ?x => x end in
     let f := match (eval pattern b in x) with ?f _ => f end in
     apply (Z.peano_ind f); intros.
     { rewrite !right_identity. reflexivity. }
-    { replace (a + Z.succ x) with ((a + x) + 1) by ring.
+    { match goal with
+      | [ |- context[?a + Z.succ ?x'] ]
+        => rename x' into x
+      end.
+      replace (a + Z.succ x) with ((a + x) + 1) by ring.
       replace (Z.succ x) with (x+1) by ring.
-      rewrite !of_Z_add_1_r, H.
+      rewrite !of_Z_add_1_r; rewrite_hyp *.
       rewrite associative; reflexivity. }
-    { replace (a + Z.pred x) with ((a+x)-1)
+    { match goal with
+      | [ |- context[?a + Z.pred ?x'] ]
+        => rename x' into x
+      end.
+      replace (a + Z.pred x) with ((a+x)-1)
         by (rewrite <-Z.sub_1_r; ring).
       replace (Z.pred x) with (x-1) by apply Z.sub_1_r.
-      rewrite !of_Z_sub_1_r, H.
+      rewrite !of_Z_sub_1_r; rewrite_hyp *.
       rewrite !ring_sub_definition.
       rewrite associative; reflexivity. }
   Qed.
@@ -382,7 +391,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 using Type*.
-    intros.
+    intros a b.
     let x := match goal with |- ?x => x end in
     let f := match (eval pattern b in x) with ?f _ => f end in
     apply (Z.peano_ind f); intros until 0; try intro IHb.
diff --git a/src/Algebra/ScalarMult.v b/src/Algebra/ScalarMult.v
index 034ed4d4c..99c1f6bbf 100644
--- a/src/Algebra/ScalarMult.v
+++ b/src/Algebra/ScalarMult.v
@@ -36,8 +36,7 @@ Section ScalarMultProperties.
 
   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).
+    induction n as [|n IHn]; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l).
   Qed.
 
   Lemma scalarmult_1_l : forall P, 1*P = P.
@@ -45,16 +44,16 @@ Section ScalarMultProperties.
 
   Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P).
   Proof using Type*.
-    induction n; intros;
+    induction n as [|n IHn]; 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 using Type*. induction m; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed.
+  Proof using Type*. induction m as [|? IHm]; 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 using Type*.
-    induction n; intros.
+    induction n as [|n IHn]; intros.
     { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. }
     { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l.
       rewrite IHn. reflexivity. }
@@ -65,7 +64,7 @@ Section ScalarMultProperties.
 
   Lemma scalarmult_mod_order : forall l B, l <> 0%nat -> l*B = zero -> forall n, n mod l * B = n * B.
   Proof using Type*.
-    intros ? ? Hnz Hmod ?.
+    intros l B Hnz Hmod n.
     rewrite (NPeano.Nat.div_mod n l Hnz) at 2.
     rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity.
   Qed.
@@ -83,7 +82,7 @@ Section ScalarMultHomomorphism.
   Lemma homomorphism_scalarmult : forall n P, phi (MUL n P) = mul n (phi P).
   Proof using Type*.
     setoid_rewrite scalarmult_ext.
-    induction n; intros; simpl; rewrite ?Monoid.homomorphism, ?IHn; easy.
+    induction n as [|n IHn]; intros; simpl; rewrite ?Monoid.homomorphism, ?IHn; easy.
   Qed.
 End ScalarMultHomomorphism.