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

60 files changed, 463 insertions, 397 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.
 
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index d651514ad..7842c1b85 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -358,7 +358,7 @@ Module B.
     Lemma split_cps_id s p: forall {T} f,
         @split_cps s p T f = f (split s p).
     Proof.
-      induction p;
+      induction p as [|?? IHp];
         repeat match goal with
                | _ => rewrite IHp
                | _ => progress (cbv [split]; prove_id)
@@ -525,9 +525,9 @@ Module B.
       Proof using Type.
         cbv [eval Associational.eval to_associational_cps zeros].
         pose proof (seq_length n 0). generalize dependent (seq 0 n).
-        intro xs; revert n; induction xs; intros;
+        intro xs; revert n; induction xs as [|?? IHxs]; intros n H;
           [autorewrite with uncps; reflexivity|].
-        intros; destruct n; [distr_length|].
+        destruct n as [|n]; [distr_length|].
         specialize (IHxs n). autorewrite with uncps in *.
         rewrite !@Tuple.to_list_repeat in *.
         simpl List.repeat. rewrite map_cons, combine_cons, map_cons.
@@ -835,7 +835,7 @@ Module B.
           eval wt (Tuple.left_append (n:=n) x xs)
           = wt n * x + eval wt xs.
       Proof.
-        induction n; intros; try destruct xs;
+        induction n as [|n IHn]; intros wt x xs; try destruct xs;
           unfold Tuple.left_append; fold @Tuple.left_append;
             autorewrite with push_basesystem_eval; [ring|].
         rewrite (Tuple.subst_append xs), Tuple.hd_append, Tuple.tl_append.
@@ -846,8 +846,8 @@ Module B.
       Lemma eval_wt_equiv {n} :forall wta wtb (x:tuple Z n),
           (forall i, wta i = wtb i) -> eval wta x = eval wtb x.
       Proof.
-        destruct n; [reflexivity|].
-        induction n; intros; [rewrite !eval_single, H; reflexivity|].
+        destruct n as [|n]; [reflexivity|].
+        induction n as [|n IHn]; intros wta wtb x H; [rewrite !eval_single, H; reflexivity|].
         simpl tuple in *; destruct x.
         change (t, z) with (Tuple.append (n:=S n) z t).
         rewrite !eval_step. rewrite (H 0%nat). apply Group.cancel_left.
@@ -879,7 +879,7 @@ Module B.
 
       Lemma map_and_0 {n} (p:tuple Z n) : Tuple.map (Z.land 0) p = zeros n.
       Proof.
-        induction n; [destruct p; reflexivity | ].
+        induction n as [|n IHn]; [destruct p; reflexivity | ].
         rewrite (Tuple.subst_append p), Tuple.map_append, Z.land_0_l, IHn.
         reflexivity.
       Qed.
diff --git a/src/Arithmetic/ModularArithmeticPre.v b/src/Arithmetic/ModularArithmeticPre.v
index 3063d3a51..ae27b290f 100644
--- a/src/Arithmetic/ModularArithmeticPre.v
+++ b/src/Arithmetic/ModularArithmeticPre.v
@@ -60,7 +60,7 @@ Qed.
 
 Lemma powmod_Zpow_mod : forall m a n, powmod m a n = (a^Z.of_N n) mod m.
 Proof.
-  induction n using N.peano_ind; [auto|].
+  induction n as [|n IHn] using N.peano_ind; [auto|].
   rewrite <-N.add_1_l.
   rewrite powmod_1plus.
   rewrite IHn.
@@ -76,7 +76,7 @@ Local Obligation Tactic := idtac.
 Program Definition pow_impl_sig {m} (a:{z : Z | z = z mod m}) (x:N) : {z : Z | z = z mod m}
   := powmod m (proj1_sig a) x.
 Next Obligation.
-  intros; destruct x; [simpl; rewrite Zmod_mod; reflexivity|].
+  intros m a x; destruct x; [simpl; rewrite Zmod_mod; reflexivity|].
   rewrite N_pos_1plus.
   rewrite powmod_1plus.
   rewrite Zmod_mod; reflexivity.
@@ -122,7 +122,7 @@ Program Definition inv_impl {m : BinNums.Z} :
     exist (fun z : BinNums.Z => z = z mod m) (1 mod m) (Z_mod_mod 1 m))}
      := mod_inv_sig.
 Next Obligation.
-  split.
+  intros m; split.
   { apply exist_reduced_eq; rewrite Zmod_0_l; reflexivity. }
   intros Hm [a pfa] Ha'. apply exist_reduced_eq.
   assert (Hm':0 <= m - 2) by (pose proof prime_ge_2 m Hm; omega).
diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v
index 8f9277f35..77186674f 100644
--- a/src/Arithmetic/ModularArithmeticTheorems.v
+++ b/src/Arithmetic/ModularArithmeticTheorems.v
@@ -104,8 +104,7 @@ Module F.
 
     Lemma of_Z_pow x n : F.of_Z _ x ^ n = F.of_Z _ (x ^ (Z.of_N n) mod m) :> F m.
     Proof using Type.
-      intros.
-      induction n using N.peano_ind;
+      induction n as [|n IHn] using N.peano_ind;
         destruct (pow_spec (F.of_Z m x)) as [pow_0 pow_succ] . {
         rewrite pow_0.
         unwrap_F; trivial.
@@ -122,9 +121,9 @@ Module F.
     Lemma to_Z_pow : forall (x : F m) n,
         F.to_Z (x ^ n)%F = (F.to_Z x ^ Z.of_N n mod m)%Z.
     Proof using Type.
-      intros.
+      intros x n.
       symmetry.
-      induction n using N.peano_ind;
+      induction n as [|n IHn] using N.peano_ind;
         destruct (pow_spec x) as [pow_0 pow_succ] . {
         rewrite pow_0, Z.pow_0_r; auto.
       } {
@@ -209,12 +208,12 @@ Module F.
 
     Lemma pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F F.mul x n.
     Proof using Type.
-      destruct (pow_spec x) as [HO HS]; intros.
-      destruct n; auto; unfold id.
+      destruct (pow_spec x) as [HO HS]; intros n.
+      destruct n as [|p]; auto; unfold id.
       rewrite ModularArithmeticPre.N_pos_1plus at 1.
       rewrite HS.
       simpl.
-      induction p using Pos.peano_ind.
+      induction p as [|p IHp] using Pos.peano_ind.
       - simpl. rewrite HO. apply Algebra.Hierarchy.right_identity.
       - rewrite (@pow_pos_succ (F m) (@F.mul m) eq _ _ associative x).
         rewrite <-IHp, Pos.pred_N_succ, ModularArithmeticPre.N_pos_1plus, HS.
@@ -229,7 +228,7 @@ Module F.
       let '(q, r) := (Z.quotrem (F.to_Z a) (F.to_Z b)) in (F.of_Z _ q , F.of_Z _ r).
     Lemma div_theory : div_theory eq (@F.add m) (@F.mul m) (@id _) quotrem.
     Proof using Type.
-      constructor; intros; unfold quotrem, id.
+      constructor; intros a b; unfold quotrem, id.
 
       replace (Z.quotrem (F.to_Z a) (F.to_Z b)) with (Z.quot (F.to_Z a) (F.to_Z b), Z.rem (F.to_Z a) (F.to_Z b)) by
           try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
@@ -245,13 +244,13 @@ Module F.
      * to inject the result afterward. *)
     Lemma ring_morph: ring_morph 0%F 1%F F.add F.mul F.sub F.opp   eq
                                  0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb  (F.of_Z m).
-    Proof using Type. split; intros; unwrap_F; solve [ auto | rewrite (proj1 (Z.eqb_eq x y)); trivial]. Qed.
+    Proof using Type. split; try intro x; try intro y; unwrap_F; solve [ auto | rewrite (proj1 (Z.eqb_eq x y)); trivial]. Qed.
 
     (* Redefine our division theory under the ring morphism *)
     Lemma morph_div_theory:
       Ring_theory.div_theory eq Zplus Zmult (F.of_Z m) Z.quotrem.
     Proof using Type.
-      split; intros.
+      split; intros a b.
       replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b);
         try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
       unwrap_F; rewrite <- (Z.quot_rem' a b); trivial.
@@ -292,7 +291,7 @@ Module F.
     Global Instance pow_is_scalarmult
       : is_scalarmult (G:=F m) (eq:=eq) (add:=F.mul) (zero:=1%F) (mul := fun n x => x ^ (N.of_nat n)).
     Proof using Type.
-      split; intros; rewrite ?Nat2N.inj_succ, <-?N.add_1_l;
+      split; [ intro P | intros n P | ]; rewrite ?Nat2N.inj_succ, <-?N.add_1_l;
         match goal with
         | [x:F m |- _ ] => solve [destruct (@pow_spec m P); auto]
         | |- Proper _ _ => solve_proper
@@ -317,7 +316,7 @@ Module F.
               match goal with
               | |- context [ (_^?n)%F ] =>
                 rewrite <-(N2Nat.id n); generalize (N.to_nat n); clear n;
-                let m := fresh n in intro m
+                intro n
               | |- context [ (_^N.of_nat ?n)%F ] =>
                 let rw := constr:(scalarmult_ext(zero:=F.of_Z m 1) n) in
                 setoid_rewrite rw (* rewriting moduloa reduction *)
diff --git a/src/Arithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v
index edab4e065..3d6260bba 100644
--- a/src/Arithmetic/PrimeFieldTheorems.v
+++ b/src/Arithmetic/PrimeFieldTheorems.v
@@ -66,9 +66,9 @@ Module F.
       rewrite F.square_iff, <-(euler_criterion (q/2)) by (trivial || omega); reflexivity.
     Qed.
 
-    Global Instance Decidable_square (x:F q) : Decidable (exists y, y*y = x).
+    Global Instance Decidable_square : forall (x:F q), Decidable (exists y, y*y = x).
     Proof.
-      destruct (dec (x = 0)).
+      intro x; destruct (dec (x = 0)).
       { left. abstract (exists 0; subst; apply Ring.mul_0_l). }
       { eapply Decidable_iff_to_impl; [eapply euler_criterion; assumption | exact _]. }
     Defined.
@@ -186,7 +186,7 @@ Module F.
 
     Lemma mul_square_sqrt_minus1 : forall x, sqrt_minus1 * x * (sqrt_minus1 * x) = F.opp (x * x).
     Proof using prime_q sqrt_minus1_valid.
-      intros.
+      intros x.
       transitivity (F.opp 1 * (x * x)); [ | field].
       rewrite <-sqrt_minus1_valid.
       field.
@@ -208,7 +208,7 @@ Module F.
     Lemma sqrt_5mod8_correct : forall x,
       ((exists y, y*y = x) <-> (sqrt_5mod8 x)*(sqrt_5mod8 x) = x).
     Proof using Type*.
-      cbv [sqrt_5mod8]; intros.
+      cbv [sqrt_5mod8]; intros x.
       destruct (F.eq_dec x 0).
       {
         repeat match goal with
diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v
index a66c268b0..880adc8f1 100644
--- a/src/Arithmetic/Saturated.v
+++ b/src/Arithmetic/Saturated.v
@@ -145,7 +145,7 @@ Module Columns.
     Lemma eval_from_S {n}: forall i (inp : (list Z)^(S n)),
         eval_from i inp = eval_from (S i) (tl inp) + weight i * sum (hd inp).
     Proof using Type.
-      intros; cbv [eval_from].
+      intros i inp; cbv [eval_from].
       replace inp with (append (hd inp) (tl inp))
         by (simpl in *; destruct n; destruct inp; reflexivity).
       rewrite map_append, B.Positional.eval_step, hd_append, tl_append.
@@ -280,7 +280,7 @@ Module Columns.
 
       apply mapi_with'_linvariant; [|tauto].
 
-      clear n inp. intros until 0. intros Hst Hys [Hmod Hdiv].
+      clear n inp. intros n st x0 xs ys Hst Hys [Hmod Hdiv].
       pose proof (weight_positive n). pose proof (weight_divides n).
       autorewrite with push_basesystem_eval.
       destruct n; cbv [mapi_with] in *; simpl tuple in *;
@@ -338,7 +338,7 @@ Module Columns.
       List.map sum (update_nth i (cons x) l) =
       update_nth i (Z.add x) (List.map sum l).
     Proof using Type.
-      induction l; intros; destruct i; simpl; rewrite ?IHl; reflexivity.
+      induction l as [|a l IHl]; intros i x; destruct i; simpl; rewrite ?IHl; reflexivity.
     Qed.
 
     Lemma cons_to_nth_add_to_nth n i x t :
@@ -367,7 +367,7 @@ Module Columns.
 
     Lemma map_sum_nils n : map sum (nils n) = B.Positional.zeros n.
     Proof using Type.
-      cbv [nils B.Positional.zeros]; induction n; [reflexivity|].
+      cbv [nils B.Positional.zeros]; induction n as [|n]; [reflexivity|].
       change (repeat nil (S n)) with (@nil Z :: repeat nil n).
       rewrite map_repeat, sum_nil. reflexivity.
     Qed.
diff --git a/src/Compilers/CommonSubexpressionEliminationWf.v b/src/Compilers/CommonSubexpressionEliminationWf.v
index 76ed1fa96..8d7bf2727 100644
--- a/src/Compilers/CommonSubexpressionEliminationWf.v
+++ b/src/Compilers/CommonSubexpressionEliminationWf.v
@@ -99,7 +99,7 @@ Section symbolic.
       : wff G' (@csef var1 t e1 m1) (@csef var2 t e2 m2).
     Proof.
       revert dependent m1; revert m2; revert dependent G'.
-      induction Hwf; simpl; intros; try constructor; auto.
+      induction Hwf; simpl; intros G' HGG' m2 m1 Hlen Hm1m2None Hm1m2Some; try constructor; auto.
       { erewrite wff_norm_symbolize_exprf by eassumption.
         break_innermost_match;
           try match goal with
@@ -170,7 +170,7 @@ Section symbolic.
           (Hwf : wff G e1 e2)
       : wff G (@prepend_prefix var1' t e1 prefix1) (@prepend_prefix var2' t e2 prefix2).
     Proof.
-      revert dependent G; revert dependent prefix2; induction prefix1, prefix2; simpl; intros; try congruence.
+      revert dependent G; revert dependent prefix2; induction prefix1, prefix2; simpl; intros Hlen Hprefix G Hwf; try congruence.
       { pose proof (Hprefix 0) as H0; specialize (fun n => Hprefix (S n)).
         destruct_head sigT; simpl in *.
         specialize (H0 _ _ _ _ eq_refl eq_refl); destruct_head ex; subst; simpl in *.
diff --git a/src/Compilers/Equality.v b/src/Compilers/Equality.v
index 8e2b44de8..2b54a7892 100644
--- a/src/Compilers/Equality.v
+++ b/src/Compilers/Equality.v
@@ -51,7 +51,7 @@ Section language.
   Lemma flat_type_dec_bl X : forall Y, flat_type_beq X Y = true -> X = Y.
   Proof. clear base_type_code_lb; induction X, Y; t. Defined.
   Lemma flat_type_dec_lb X : forall Y, X = Y -> flat_type_beq X Y = true.
-  Proof. clear base_type_code_bl; intros; subst Y; induction X; t. Defined.
+  Proof. clear base_type_code_bl; intros Y **; subst Y; induction X; t. Defined.
   Definition flat_type_eq_dec (X Y : flat_type) : {X = Y} + {X <> Y}
     := match Sumbool.sumbool_of_bool (flat_type_beq X Y) with
        | left pf => left (flat_type_dec_bl _ _ pf)
@@ -65,7 +65,7 @@ Section language.
   Lemma type_dec_bl X : forall Y, type_beq X Y = true -> X = Y.
   Proof. clear base_type_code_lb; pose proof flat_type_dec_bl; induction X, Y; t. Defined.
   Lemma type_dec_lb X : forall Y, X = Y -> type_beq X Y = true.
-  Proof. clear base_type_code_bl; pose proof flat_type_dec_lb; intros; subst Y; induction X; t. Defined.
+  Proof. clear base_type_code_bl; pose proof flat_type_dec_lb; intros Y **; subst Y; induction X; t. Defined.
   Definition type_eq_dec (X Y : type) : {X = Y} + {X <> Y}
     := match Sumbool.sumbool_of_bool (type_beq X Y) with
        | left pf => left (type_dec_bl _ _ pf)
diff --git a/src/Compilers/MapCastByDeBruijnInterp.v b/src/Compilers/MapCastByDeBruijnInterp.v
index 10e09242a..7674e5f0e 100644
--- a/src/Compilers/MapCastByDeBruijnInterp.v
+++ b/src/Compilers/MapCastByDeBruijnInterp.v
@@ -66,6 +66,7 @@ Section language.
                         then fun pf => left (base_type_code_bl_transparent _ _ pf)
                         else fun pf => right _) eq_refl).
     { clear -pf base_type_code_lb.
+      let pf := pf in
       abstract (intro; erewrite base_type_code_lb in pf by eassumption; congruence). }
   Defined.
 
diff --git a/src/Compilers/MapCastByDeBruijnWf.v b/src/Compilers/MapCastByDeBruijnWf.v
index 7c1e386b5..61a084ee7 100644
--- a/src/Compilers/MapCastByDeBruijnWf.v
+++ b/src/Compilers/MapCastByDeBruijnWf.v
@@ -64,6 +64,7 @@ Section language.
                         then fun pf => left (base_type_code_bl_transparent _ _ pf)
                         else fun pf => right _) eq_refl).
     { clear -pf base_type_code_lb.
+      let pf := pf in
       abstract (intro; erewrite base_type_code_lb in pf by eassumption; congruence). }
   Defined.
 
diff --git a/src/Compilers/Named/ContextProperties/NameUtil.v b/src/Compilers/Named/ContextProperties/NameUtil.v
index 0bc970357..320d910f0 100644
--- a/src/Compilers/Named/ContextProperties/NameUtil.v
+++ b/src/Compilers/Named/ContextProperties/NameUtil.v
@@ -47,7 +47,7 @@ Section with_context.
     : (exists t, @find_Name n T N = Some t)
       <-> List.In (Some n) (List.firstn (CountLets.count_pairs T) ls).
   Proof using Type.
-    revert dependent ls; intro ls; revert ls ls'; induction T; intros;
+    revert dependent ls; intro ls; revert ls ls'; induction T; intros ls ls' H;
       [ | | specialize (IHT1 (fst N) ls (snd (split_onames T1 ls)));
             specialize (IHT2 (snd N) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ];
       repeat first [ misc_oname_t_step
@@ -77,7 +77,11 @@ Section with_context.
     rewrite fst_split_onames_firstn, snd_split_onames_skipn in H.
     inversion_prod; subst.
     split; [ split | intros [? ?] ]; eauto using In_firstn, oname_list_unique_specialize.
-    eapply In_firstn_skipn_split in H; destruct_head' or; eauto; exfalso; eauto.
+    match goal with
+    | [ H : List.In (Some _) ?ls |- _ ]
+      => is_var ls;
+           eapply In_firstn_skipn_split in H; destruct_head' or; eauto; exfalso; eauto
+    end.
   Qed.
 
   Lemma split_onames_find_Name_Some_unique
@@ -97,7 +101,7 @@ Section with_context.
     : @find_Name_and_val var' t n T N V None = Some v
       <-> List.In (existT (fun t => (Name * var' t)%type) t (n, v)) (Wf.flatten_binding_list N V).
   Proof using Type.
-    revert dependent ls; intro ls; revert ls ls'; induction T; intros;
+    revert dependent ls; intro ls; revert ls ls'; induction T; intros ls ls' Hls H;
       [ | | specialize (IHT1 (fst N) (fst V) ls (snd (split_onames T1 ls)));
             specialize (IHT2 (snd N) (snd V) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ];
       repeat first [ find_Name_and_val_default_to_None_step
diff --git a/src/Compilers/Named/ContextProperties/Proper.v b/src/Compilers/Named/ContextProperties/Proper.v
index 48cecde8f..0c583e446 100644
--- a/src/Compilers/Named/ContextProperties/Proper.v
+++ b/src/Compilers/Named/ContextProperties/Proper.v
@@ -41,15 +41,15 @@ Section with_context.
                  | rewrite lookupb_removeb_different by assumption
                  | solve [ auto ] ].
 
-  Global Instance extendb_Proper {t} : Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extendb t) | 10.
+  Global Instance extendb_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extendb t) | 10.
   Proof.
-    intros ??? n n0 ???? n' t'; subst n0; subst; proper_t n n' t t'.
+    intros t ??? n n0 ???? n' t'; subst n0; subst; proper_t n n' t t'.
   Qed.
-  Global Instance removeb_Proper {t} : Proper (context_equiv ==> eq ==> context_equiv) (@removeb t) | 10.
+  Global Instance removeb_Proper : forall {t}, Proper (context_equiv ==> eq ==> context_equiv) (@removeb t) | 10.
   Proof.
-    intros ??? n n0 ? n' t'; subst n0; subst; proper_t n n' t t'.
+    intros t ??? n n0 ? n' t'; subst n0; subst; proper_t n n' t t'.
   Qed.
-  Global Instance lookupb_Proper {t} : Proper (context_equiv ==> eq ==> eq) (@lookupb t) | 10.
+  Global Instance lookupb_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq) (@lookupb t) | 10.
   Proof. repeat intro; subst; auto. Qed.
 
   Local Ltac proper_t2 t :=
@@ -68,13 +68,14 @@ Section with_context.
       first [ eapply IHt2; [ eapply IHt1 | .. ]; auto
             | idtac ] ].
 
-  Global Instance extend_Proper {t} : Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extend t) | 10.
-  Proof. proper_t2 t. Qed.
-  Global Instance remove_Proper {t} : Proper (context_equiv ==> eq ==> context_equiv) (@remove t) | 10.
-  Proof. proper_t2 t. Qed.
-  Global Instance lookup_Proper {t} : Proper (context_equiv ==> eq ==> eq) (@lookup t) | 10.
+  Global Instance extend_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq ==> context_equiv) (@extend t) | 10.
+  Proof. intro t; proper_t2 t. Qed.
+  Global Instance remove_Proper : forall {t}, Proper (context_equiv ==> eq ==> context_equiv) (@remove t) | 10.
+  Proof. intro t; proper_t2 t. Qed.
+
+  Global Instance lookup_Proper : forall {t}, Proper (context_equiv ==> eq ==> eq) (@lookup t) | 10.
   Proof.
-    proper_t2 t.
+    intro t; proper_t2 t.
     repeat match goal with
            | [ |- context G[lookup (?A * ?B) ?ctx (?na, ?nb)] ]
              => let G' := context G[match lookup A ctx na, lookup B ctx nb with
@@ -88,7 +89,7 @@ Section with_context.
              | _ => progress subst
              | _ => progress inversion_option
              | _ => reflexivity
-             | [ H : lookup _ _ _ = ?x, H' : lookup _ _ _ = ?y |- _ ]
+             | [ IHt2 : Proper _ (lookup t2), H : lookup _ _ _ = ?x, H' : lookup _ _ _ = ?y |- _ ]
                => assert (x = y)
                  by (rewrite <- H, <- H'; first [ eapply IHt1 | eapply IHt2 ]; (assumption || reflexivity));
                     clear H H'
diff --git a/src/Compilers/Named/NameUtilProperties.v b/src/Compilers/Named/NameUtilProperties.v
index d2791a5ea..944d164f2 100644
--- a/src/Compilers/Named/NameUtilProperties.v
+++ b/src/Compilers/Named/NameUtilProperties.v
@@ -171,7 +171,7 @@ Section language.
         (t : flat_type base_type_code) (ls : list Name)
     : fst (split_names t ls) <> None <-> List.length ls >= count_pairs t.
   Proof using Type.
-    revert ls; induction t; intros;
+    revert ls; induction t; intros ls;
       try solve [ destruct ls; simpl; intuition (omega || congruence) ].
     repeat first [ progress simpl in *
                  | progress break_innermost_match_step
diff --git a/src/Compilers/TestCase.v b/src/Compilers/TestCase.v
index 36774e4e3..e1fb0087a 100644
--- a/src/Compilers/TestCase.v
+++ b/src/Compilers/TestCase.v
@@ -212,17 +212,17 @@ Module bounds.
   Definition add_bounded_pf (x y : bounded_pf) : bounded_pf.
   Proof.
     exists (map_bounded_f2 plus false (proj1_sig x) (proj1_sig y)).
-    simpl; abstract (destruct x, y; simpl; omega).
+    simpl; let x := x in let y := y in abstract (destruct x, y; simpl; omega).
   Defined.
   Definition mul_bounded_pf (x y : bounded_pf) : bounded_pf.
   Proof.
     exists (map_bounded_f2 mult false (proj1_sig x) (proj1_sig y)).
-    simpl; abstract (destruct x, y; simpl; nia).
+    simpl; let x := x in let y := y in abstract (destruct x, y; simpl; nia).
   Defined.
   Definition sub_bounded_pf (x y : bounded_pf) : bounded_pf.
   Proof.
     exists (map_bounded_f2 minus true (proj1_sig x) (proj1_sig y)).
-    simpl; abstract (destruct x, y; simpl; omega).
+    simpl; let x := x in let y := y in abstract (destruct x, y; simpl; omega).
   Defined.
   Definition interp_base_type_bounds (v : base_type) : Type :=
     match v with
diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v
index ba5dd39cd..56dda81ab 100644
--- a/src/Compilers/Z/ArithmeticSimplifierWf.v
+++ b/src/Compilers/Z/ArithmeticSimplifierWf.v
@@ -115,7 +115,8 @@ Lemma wff_interp_as_expr_or_const_base {var1 var2 t} {G e1 e2 v1 v2}
        end.
 Proof.
   invert_one_expr e1; intros; break_innermost_match; intros;
-    try invert_one_expr e2; intros;
+    try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in
+         invert_one_expr e2); intros;
       repeat first [ fin_t
                    | progress simpl in *
                    | progress intros
@@ -157,7 +158,9 @@ Lemma wff_interp_as_expr_or_const_prod_base {var1 var2 A B} {G e1 e2} {v1 v2 : _
           end.
 Proof.
   invert_one_expr e1; intros; break_innermost_match; intros; try exact I;
-    try invert_one_expr e2; intros; break_innermost_match; intros; try exact I;
+    try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in
+         invert_one_expr e2);
+    intros; break_innermost_match; intros; try exact I;
       repeat first [ pret_step
                    | pose_wff_base
                    | break_t_step
@@ -206,7 +209,9 @@ Lemma wff_interp_as_expr_or_const_prod3_base {var1 var2 A B C} {G e1 e2} {v1 v2
           end.
 Proof.
   invert_one_expr e1; intros; break_innermost_match; intros; try exact I;
-    try invert_one_expr e2; intros; break_innermost_match; intros; try exact I;
+    try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in
+         invert_one_expr e2);
+    intros; break_innermost_match; intros; try exact I;
       repeat first [ pret_step
                    | pose_wff_base
                    | pose_wff_prod
diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v
index dc29fe654..882cbde3a 100644
--- a/src/Compilers/Z/Bounds/Interpretation.v
+++ b/src/Compilers/Z/Bounds/Interpretation.v
@@ -288,7 +288,7 @@ Module Import Bounds.
     := interp_flat_type_rel_pointwise (@is_bounded_by').
 
   Local Arguments interp_base_type !_ / .
-  Global Instance dec_eq_interp_flat_type {T} : DecidableRel (@eq (interp_flat_type interp_base_type T)) | 10.
+  Global Instance dec_eq_interp_flat_type : forall {T}, DecidableRel (@eq (interp_flat_type interp_base_type T)) | 10.
   Proof.
     induction T; destruct_head base_type; simpl; exact _.
   Defined.
diff --git a/src/Curves/Edwards/AffineProofs.v b/src/Curves/Edwards/AffineProofs.v
index e77e39f50..8e69b78fe 100644
--- a/src/Curves/Edwards/AffineProofs.v
+++ b/src/Curves/Edwards/AffineProofs.v
@@ -44,7 +44,7 @@ Module E.
     Local Notation mul   := (E.mul(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
 
     Program Definition opp (P:point) : point := (Fopp (fst P), (snd P)).
-    Next Obligation. destruct P as [ [??]?]; cbv; fsatz. Qed.
+    Next Obligation. match goal with P : point |- _ => destruct P as [ [??]?] end; cbv; fsatz. Qed.
 
     Ltac t_step :=
       match goal with
@@ -203,7 +203,10 @@ Module E.
         cbv [compress decompress exist_option coordinates] in *; intros.
         t.
         intro.
-        apply (H0 f); [|congruence].
+        match goal with
+        | [ H0 : _ |- False ]
+          => apply (H0 f); [|congruence]
+        end.
         admit.
         intro. Prod.inversion_prod; subst.
         rewrite solve_correct in y.
diff --git a/src/Curves/Edwards/XYZT.v b/src/Curves/Edwards/XYZT.v
index 2b126dfcb..3604e9b2e 100644
--- a/src/Curves/Edwards/XYZT.v
+++ b/src/Curves/Edwards/XYZT.v
@@ -105,7 +105,12 @@ Module Extended.
           let Z3 := F*G in
           (X3, Y3, Z3, T3)
         end.
-      Next Obligation. pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1))  _ _  (proj2_sig (to_twisted P2))); t. Qed.
+      Next Obligation.
+        match goal with
+        | [ |- match (let (_, _) := coordinates ?P1 in let (_, _) := _ in let (_, _) := _ in let (_, _) := coordinates ?P2 in _) with _ => _ end ]
+          => pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1))  _ _  (proj2_sig (to_twisted P2)))
+        end; t.
+      Qed.
 
       Global Instance isomorphic_commutative_group_m1 :
         @Group.isomorphic_commutative_groups
diff --git a/src/Curves/Montgomery/Affine.v b/src/Curves/Montgomery/Affine.v
index bfd7dce60..2e39c6b6c 100644
--- a/src/Curves/Montgomery/Affine.v
+++ b/src/Curves/Montgomery/Affine.v
@@ -2,6 +2,7 @@ Require Import Crypto.Algebra.Field.
 Require Import Crypto.Util.GlobalSettings.
 Require Import Crypto.Util.Sum Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Spec.MontgomeryCurve Crypto.Spec.WeierstrassCurve.
 
 Module M.
@@ -30,7 +31,7 @@ Module M.
       | (x, y) => (x, -y)
       | ∞ => ∞
       end.
-    Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+    Next Obligation. Proof. destruct_head @M.point; cbv; break_match; trivial; fsatz. Qed.
 
     Local Notation add := (M.add(b_nonzero:=b_nonzero)).
     Local Notation point := (@M.point F Feq Fadd Fmul a b).
@@ -52,14 +53,14 @@ Module M.
         | (x, y) => ((x + a/3)/b, y/b)
         | _ => ∞
         end.
-      Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+      Next Obligation. Proof. destruct_head' @point; cbv; break_match; trivial; fsatz. Qed.
 
       Program Definition of_Weierstrass (P:Wpoint) : point :=
         match W.coordinates P return F*F+∞ with
         | (x,y) => (b*x-a/3, b*y)
         | _ => ∞
         end.
-      Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+      Next Obligation. Proof. destruct_head' @Wpoint; cbv; break_match; trivial; fsatz. Qed.
     End MontgomeryWeierstrass.
   End MontgomeryCurve.
 End M.
diff --git a/src/Curves/Weierstrass/Projective.v b/src/Curves/Weierstrass/Projective.v
index 20866ca5d..3c1fd204d 100644
--- a/src/Curves/Weierstrass/Projective.v
+++ b/src/Curves/Weierstrass/Projective.v
@@ -123,8 +123,11 @@ Module Projective.
       end.
     Next Obligation.
     Proof.
-      destruct P as [p ?]; destruct p as [p Z1]; destruct p as [X1 Y1].
-      destruct Q as [q ?]; destruct q as [q Z2]; destruct q as [X2 Y2].
+      match goal with
+      | [ |- match (let (_, _) := proj1_sig ?P in let (_, _) := _ in let (_, _) := proj1_sig ?Q in _) with _ => _ end ]
+        => destruct P as [p ?]; destruct p as [p Z1]; destruct p as [X1 Y1];
+             destruct Q as [q ?]; destruct q as [q Z2]; destruct q as [X2 Y2]
+      end.
       t.
       all: try abstract fsatz.
       (* FIXME: the final fsatz starts requiring 56 <> 0 if
diff --git a/src/LegacyArithmetic/BaseSystemProofs.v b/src/LegacyArithmetic/BaseSystemProofs.v
index b87df814d..f0f0a80d2 100644
--- a/src/LegacyArithmetic/BaseSystemProofs.v
+++ b/src/LegacyArithmetic/BaseSystemProofs.v
@@ -122,7 +122,8 @@ Section BaseSystemProofs.
              end.
     rewrite (combine_truncate_r vs bs); apply (f_equal2 Z.add); trivial; [].
     unfold combine; break_match.
-    { apply (f_equal (@length _)) in Heql; simpl length in Heql; rewrite skipn_length in Heql; omega. }
+    { let Heql := match goal with H : _ = nil |- _ => H end in
+      apply (f_equal (@length _)) in Heql; simpl length in Heql; rewrite skipn_length in Heql; omega. }
     { cbv -[Z.add Z.mul]; ring_simplify; f_equal.
       assert (HH: nth_error (z0 :: l) 0 = Some z) by
           (
diff --git a/src/LegacyArithmetic/Double/Proofs/Decode.v b/src/LegacyArithmetic/Double/Proofs/Decode.v
index b5b6d6623..1cd5bf06d 100644
--- a/src/LegacyArithmetic/Double/Proofs/Decode.v
+++ b/src/LegacyArithmetic/Double/Proofs/Decode.v
@@ -145,9 +145,10 @@ Hint Rewrite
 
 Hint Rewrite @tuple_decoder_S @tuple_decoder_O @tuple_decoder_m1 using solve [ auto with zarith ] : simpl_tuple_decoder.
 
-Global Instance tuple_decoder_mod {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k)))
-  : tuple_decoder (k := S k) (fst w) <~= tuple_decoder w mod 2^(S k * n).
+Global Instance tuple_decoder_mod : forall {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k))),
+    tuple_decoder (k := S k) (fst w) <~= tuple_decoder w mod 2^(S k * n).
 Proof.
+  intros n W decode k isdecode w.
   pose proof (snd w).
   assert (0 <= n) by eauto using decode_exponent_nonnegative.
   assert (0 <= (S k) * n) by nia.
@@ -156,9 +157,10 @@ Proof.
   reflexivity.
 Qed.
 
-Global Instance tuple_decoder_div {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k)))
-  : decode (snd w) <~= tuple_decoder w / 2^(S k * n).
+Global Instance tuple_decoder_div : forall {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k))),
+    decode (snd w) <~= tuple_decoder w / 2^(S k * n).
 Proof.
+  intros n W decode k isdecode w.
   pose proof (snd w).
   assert (0 <= n) by eauto using decode_exponent_nonnegative.
   assert (0 <= (S k) * n) by nia.
@@ -169,16 +171,18 @@ Proof.
   reflexivity.
 Qed.
 
-Global Instance tuple2_decoder_mod {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2)
-  : decode (fst w) <~= tuple_decoder w mod 2^n.
+Global Instance tuple2_decoder_mod : forall {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2),
+    decode (fst w) <~= tuple_decoder w mod 2^n.
 Proof.
+  intros n W decode isdecode w.
   generalize (@tuple_decoder_mod n W decode 0 isdecode w).
   autorewrite with simpl_tuple_decoder; trivial.
 Qed.
 
-Global Instance tuple2_decoder_div {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2)
-  : decode (snd w) <~= tuple_decoder w / 2^n.
+Global Instance tuple2_decoder_div : forall {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2),
+    decode (snd w) <~= tuple_decoder w / 2^n.
 Proof.
+  intros n W decode isdecode w.
   generalize (@tuple_decoder_div n W decode 0 isdecode w).
   autorewrite with simpl_tuple_decoder; trivial.
 Qed.
diff --git a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v
index e703c2e57..d0514db57 100644
--- a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v
+++ b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v
@@ -122,12 +122,13 @@ Section ripple_carry_adc.
   Proof using Type. apply ripple_carry_tuple_SS. Qed.
 
   Local Opaque Z.of_nat.
-  Global Instance ripple_carry_is_add_with_carry {k}
-         {isdecode : is_decode decode}
-         {is_adc : is_add_with_carry adc}
-    : is_add_with_carry (ripple_carry_adc (k := k) adc).
+  Global Instance ripple_carry_is_add_with_carry
+    : forall {k}
+             {isdecode : is_decode decode}
+             {is_adc : is_add_with_carry adc},
+      is_add_with_carry (ripple_carry_adc (k := k) adc).
   Proof using Type.
-    destruct k as [|k].
+    destruct k as [|k]; intros isdecode is_adc.
     { constructor; simpl; intros; autorewrite with zsimplify; reflexivity. }
     { induction k as [|k IHk].
       { cbv [ripple_carry_adc ripple_carry_tuple to_list].
@@ -166,12 +167,13 @@ Section ripple_carry_subc.
   Proof using Type. apply ripple_carry_tuple_SS. Qed.
 
   Local Opaque Z.of_nat.
-  Global Instance ripple_carry_is_sub_with_carry {k}
-         {isdecode : is_decode decode}
-         {is_subc : is_sub_with_carry subc}
-    : is_sub_with_carry (ripple_carry_subc (k := k) subc).
+  Global Instance ripple_carry_is_sub_with_carry
+    : forall {k}
+             {isdecode : is_decode decode}
+             {is_subc : is_sub_with_carry subc},
+      is_sub_with_carry (ripple_carry_subc (k := k) subc).
   Proof using Type.
-    destruct k as [|k].
+    destruct k as [|k]; intros isdecode is_subc.
     { constructor; repeat (intros [] || intro); autorewrite with simpl_tuple_decoder zsimplify; reflexivity. }
     { induction k as [|k IHk].
       { cbv [ripple_carry_subc ripple_carry_tuple to_list].
diff --git a/src/LegacyArithmetic/InterfaceProofs.v b/src/LegacyArithmetic/InterfaceProofs.v
index 9ef97fa55..33917e00d 100644
--- a/src/LegacyArithmetic/InterfaceProofs.v
+++ b/src/LegacyArithmetic/InterfaceProofs.v
@@ -99,8 +99,9 @@ Global Instance decode_proj n W (dec : W -> Z)
   : @decode n W {| decode := dec |} =~> dec.
 Proof. reflexivity. Qed.
 
-Global Instance decode_if_bool n W (decode : decoder n W) (b : bool) x y
-  : decode (if b then x else y)
+Global Instance decode_if_bool n W (decode : decoder n W)
+  : forall (b : bool) x y,
+    decode (if b then x else y)
     =~> if b then decode x else decode y.
 Proof. destruct b; reflexivity. Qed.
 
diff --git a/src/LegacyArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v
index 35540f39a..b6df85f5c 100644
--- a/src/LegacyArithmetic/Pow2BaseProofs.v
+++ b/src/LegacyArithmetic/Pow2BaseProofs.v
@@ -73,7 +73,7 @@ Section Pow2BaseProofs.
     nth_error base (S i) = Some (two_p w * b).
   Proof using Type.
     clear limb_widths_nonneg. (* don't use this in the inductive hypothesis *)
-    induction limb_widths; intros ? ? ? ? nth_err_w nth_err_b;
+    induction limb_widths; intros i b w ? nth_err_w nth_err_b;
       unfold base_from_limb_widths in *; fold base_from_limb_widths in *;
       [rewrite (@nil_length0 Z) in *; omega | ].
     simpl in *.
@@ -97,7 +97,7 @@ Section Pow2BaseProofs.
   Lemma nth_error_base : forall i, (i < length limb_widths)%nat ->
     nth_error base i = Some (two_p (sum_firstn limb_widths i)).
   Proof using Type*.
-    induction i; intros.
+    induction i as [|i IHi]; intros H.
     + unfold sum_firstn, base_from_limb_widths in *; case_eq limb_widths; try reflexivity.
       intro lw_nil; rewrite lw_nil, (@nil_length0 Z) in *; omega.
     + assert (i < length limb_widths)%nat as lt_i_length by omega.
@@ -165,6 +165,7 @@ Section Pow2BaseProofs.
                                           Z.pow2_mod (nth_default 0 us i) (nth_default 0 lw i) = nth_default 0 us i.
   Proof using Type.
     clear.
+    cbv [bounded]; intros lw us i H H0.
     repeat match goal with
            | |- _ => progress (cbv [bounded]; intros)
            | |- _ => break_if
@@ -174,6 +175,7 @@ Section Pow2BaseProofs.
            end.
     specialize (H0 i).
     symmetry.
+    let n := match goal with n : Z |- _ => n end in
     rewrite <- (Z.mod_pow2_bits_high (nth_default 0 us i) (nth_default 0 lw i) n);
       [ rewrite Z.mod_small by omega; reflexivity | ].
     split; try omega.
@@ -183,15 +185,15 @@ Section Pow2BaseProofs.
   Lemma bounded_nil_iff : forall us, bounded nil us <-> (forall u, In u us -> u = 0).
   Proof using Type.
     clear.
-    split; cbv [bounded]; intros.
-    + edestruct (In_nth_error_value us u); try assumption.
+    intros us; split; cbv [bounded]; [ intros H u H0 | intros H i ].
+    + edestruct (In_nth_error_value us u) as [x]; try assumption.
       specialize (H x).
       replace u with (nth_default 0 us x) by (auto using nth_error_value_eq_nth_default).
       rewrite nth_default_nil, Z.pow_0_r in H.
       omega.
     + rewrite nth_default_nil, Z.pow_0_r.
       apply nth_default_preserves_properties; try omega.
-      intros.
+      intros x H0.
       apply H in H0.
       omega.
   Qed.
@@ -206,7 +208,8 @@ Section Pow2BaseProofs.
   Lemma digit_select : forall us i, bounded limb_widths us ->
                                     nth_default 0 us i = Z.pow2_mod (BaseSystem.decode base us >> sum_firstn limb_widths i) (nth_default 0 limb_widths i).
   Proof using Type*.
-    intro; revert limb_widths limb_widths_nonneg; induction us; intros.
+    intro us; revert limb_widths limb_widths_nonneg; induction us as [|a us IHus];
+      intros limb_widths limb_widths_nonneg i H.
     + rewrite nth_default_nil, BaseSystemProofs.decode_nil, Z.shiftr_0_l, Z.pow2_mod_spec, Z.mod_0_l by
           (try (apply Z.pow_nonzero; try omega); apply nth_default_preserves_properties; auto; omega).
       reflexivity.
@@ -226,7 +229,7 @@ Section Pow2BaseProofs.
           rewrite bounded_iff in *.
           specialize (H 0%nat); rewrite !nth_default_cons in H.
           rewrite <-Z.lor_shiftl by (auto using in_eq; omega).
-          apply Z.bits_inj'; intros.
+          apply Z.bits_inj'; intros n H0.
           rewrite Z.testbit_pow2_mod by auto using in_eq.
           break_if. {
             autorewrite with Ztestbit; break_match;
@@ -270,7 +273,7 @@ Section Pow2BaseProofs.
     bounded limb_widths us ->
     BaseSystem.decode' base (firstn i us) = Z.pow2_mod (BaseSystem.decode' base us) (sum_firstn limb_widths i).
   Proof using Type*.
-    intros; induction i;
+    intros us i H H0 H1; induction i;
     repeat match goal with
            | |- _ => rewrite sum_firstn_0, BaseSystemProofs.decode_nil, Z.pow2_mod_0_r; reflexivity
            | |- _ => progress distr_length
@@ -325,7 +328,7 @@ Section Pow2BaseProofs.
     sum_firstn limb_widths (length us) <= n ->
     Z.testbit (BaseSystem.decode base us) n = false.
   Proof using Type*.
-    intros.
+    intros us n H H0 H1.
     erewrite <-(firstn_all _ us) by reflexivity.
     auto using testbit_decode_firstn_high.
   Qed.
@@ -336,7 +339,7 @@ Section Pow2BaseProofs.
     bounded limb_widths us ->
     0 <= BaseSystem.decode base us.
   Proof using Type*.
-    intros.
+    intros us H H0.
     unfold bounded, BaseSystem.decode, BaseSystem.decode' in *; simpl in *.
     pose 0 as zero.
     assert (0 <= zero) by reflexivity.
@@ -365,7 +368,7 @@ Section Pow2BaseProofs.
     bounded limb_widths us ->
     0 <= BaseSystem.decode base us < upper_bound limb_widths.
   Proof using Type*.
-    cbv [upper_bound]; intros.
+    cbv [upper_bound]; intros us H H0.
     split.
     { apply decode_nonneg; auto. }
     { apply Z.testbit_false_bound; auto; intros.
@@ -387,7 +390,7 @@ Section Pow2BaseProofs.
   Lemma decode_shift : forall us u0, (length (u0 :: us) <= length limb_widths)%nat ->
     BaseSystem.decode base (u0 :: us) = u0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << (nth_default 0 limb_widths 0)).
   Proof using Type*.
-    intros; etransitivity; [ apply (decode_shift_app (u0::nil)); assumption | ].
+    intros us u0 H; etransitivity; [ apply (decode_shift_app (u0::nil)); assumption | ].
     transitivity (u0 * 1 + 0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << (nth_default 0 limb_widths 0 + 0))); [ | autorewrite with zsimplify; reflexivity ].
     destruct limb_widths; distr_length; reflexivity.
   Qed.
@@ -437,10 +440,10 @@ Section UniformBase.
    Lemma bounded_uniform : forall us, (length us <= length limb_widths)%nat ->
      (bounded limb_widths us <-> (forall u, In u us -> 0 <= u < 2 ^ width)).
    Proof using Type*.
-     cbv [bounded]; split; intro A; intros.
+     cbv [bounded]; intros us H; split; intro A; [ intros u H0 | intros i ].
      + let G := fresh "G" in
        match goal with H : In _ us |- _ =>
-         eapply In_nth in H; destruct H as [? G]; destruct G as [? G];
+         eapply In_nth in H; destruct H as [x G]; destruct G as [? G];
          rewrite <-nth_default_eq in G; rewrite <-G end.
        specialize (A x).
        split; try eapply A.
@@ -457,7 +460,7 @@ Section UniformBase.
 
   Lemma uniform_limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w.
   Proof using Type*.
-    intros.
+    intros w H.
     replace w with width by (symmetry; auto).
     assumption.
   Qed.
@@ -502,7 +505,7 @@ Section UniformBase.
   Lemma decode_truncate_base : forall us bs, BaseSystem.decode bs us = BaseSystem.decode (firstn (length us) bs) us.
   Proof using Type.
     clear.
-    induction us; intros.
+    induction us as [|a us IHus]; intros bs.
     + rewrite !BaseSystemProofs.decode_nil; reflexivity.
     + distr_length.
       destruct bs.
@@ -517,7 +520,7 @@ Section UniformBase.
                                              (n < length xs)%nat ->
                                              firstn n xs = firstn n (tl xs).
   Proof using Type.
-    intros.
+    intros A xs n x H H0.
     erewrite (repeat_spec_eq xs) by first [ eassumption | reflexivity ].
     rewrite ListUtil.tl_repeat.
     autorewrite with push_firstn.
diff --git a/src/Primitives/EdDSARepChange.v b/src/Primitives/EdDSARepChange.v
index 1ad4611be..1c6282fb9 100644
--- a/src/Primitives/EdDSARepChange.v
+++ b/src/Primitives/EdDSARepChange.v
@@ -60,7 +60,7 @@ Section EdDSA.
   Definition verify'_sig : { verify | forall mlen (message:word mlen) (pk:word b) (sig:word (b+b)),
       verify mlen message pk sig = true <-> valid message pk sig }.
   Proof.
-    eexists; intros; set_evars.
+    eexists; intros mlen message pk sig; set_evars.
     unfold Spec.EdDSA.valid.
     setoid_rewrite solve_for_R.
     setoid_rewrite combine_eq_iff.
diff --git a/src/Primitives/MxDHRepChange.v b/src/Primitives/MxDHRepChange.v
index 9f0276ef8..eb3df559a 100644
--- a/src/Primitives/MxDHRepChange.v
+++ b/src/Primitives/MxDHRepChange.v
@@ -100,7 +100,7 @@ Section MxDHRepChange.
          R (proj (fold_left step xs init)) (fold_left step' xs init').
   Proof using Type.
     generalize dependent init; generalize dependent init'.
-    induction xs; [solve [eauto]|].
+    induction xs as [|?? IHxs]; [solve [eauto]|].
     repeat intro; simpl; rewrite IHxs by eauto.
     apply (_ : Proper ((R ==> eq ==> R) ==> SetoidList.eqlistA eq ==> R ==> R) (@fold_left _ _));
       try reflexivity;
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 9cde8d004..de3bbb011 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -39,7 +39,7 @@ Module E.
         (x1, y1), (x2, y2) =>
         (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))
       end.
-    Next Obligation. destruct P1 as [[??]?], P2 as [[??]?]; eapply Pre.onCurve_add; eauto. Qed.
+    Next Obligation. do 2 match goal with P : point |- _ => destruct P as [[??]?] end; eapply Pre.onCurve_add; eauto. Qed.
 
     Fixpoint mul (n:nat) (P : point) : point :=
       match n with
diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v
index d9e801a0c..fa520f16c 100644
--- a/src/Specific/ArithmeticSynthesisTest.v
+++ b/src/Specific/ArithmeticSynthesisTest.v
@@ -115,7 +115,7 @@ Section Ops51.
                  let eval := Positional.Fdecode (m:=m) wt in
                  eval (add a b) = (eval a  + eval b)%F }.
   Proof.
-    eexists; cbv beta zeta; intros.
+    eexists; cbv beta zeta; intros a b.
     pose proof wt_nonzero.
     let x := constr:(
         Positional.add_cps (n := sz) wt a b id) in
@@ -128,7 +128,7 @@ Section Ops51.
                  let eval := Positional.Fdecode (m:=m) wt in
                  eval (sub a b) = (eval a - eval b)%F}.
   Proof.
-    eexists; cbv beta zeta; intros.
+    eexists; cbv beta zeta; intros a b.
     pose proof wt_nonzero.
     let x := constr:(
          Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in
@@ -141,7 +141,7 @@ Section Ops51.
                  let eval := Positional.Fdecode (m := m) wt in
                  eval (opp a) = F.opp (eval a)}.
   Proof.
-    eexists; cbv beta zeta; intros.
+    eexists; cbv beta zeta; intros a.
     pose proof wt_nonzero.
     let x := constr:(
          Positional.opp_cps (n:=sz) (coef := coef) wt a id) in
@@ -154,7 +154,7 @@ Section Ops51.
                  let eval := Positional.Fdecode (m := m) wt in
                  eval (mul a b) = (eval a  * eval b)%F}.
   Proof.
-    eexists; cbv beta zeta; intros.
+    eexists; cbv beta zeta; intros a b.
     pose proof wt_nonzero.
     let x := constr:(
          Positional.mul_cps (n:=sz) (m:=sz2) wt a b
@@ -190,7 +190,7 @@ Section Ops51.
                  let eval := Positional.Fdecode (m := m) wt in
                  eval (square a) = (eval a  * eval a)%F}.
   Proof.
-    eexists; cbv beta zeta; intros.
+    eexists; cbv beta zeta; intros a.
     pose proof wt_nonzero.
     let x := constr:(
          Positional.mul_cps (n:=sz) (m:=sz2) wt a a
@@ -221,7 +221,7 @@ Section Ops51.
                  let eval := Positional.Fdecode (m := m) wt in
                  eval (carry a) = eval a}.
   Proof.
-    eexists; cbv beta zeta; intros.
+    eexists; cbv beta zeta; intros a.
     pose proof wt_nonzero. pose proof wt_divides_chain1.
     pose proof div_mod. pose proof wt_divides_chain2.
     let x := constr:(
@@ -262,7 +262,7 @@ Section Ops51.
                  let eval := Positional.Fdecode (m := m) wt in
                  eval (freeze a) = eval a}.
   Proof.
-    eexists; cbv beta zeta; intros.
+    eexists; cbv beta zeta; intros a ?.
     pose proof wt_nonzero. pose proof wt_pos.
     pose proof div_mod. pose proof wt_divides_full_pos.
     pose proof wt_multiples.
diff --git a/src/Specific/ArithmeticSynthesisTest130.v b/src/Specific/ArithmeticSynthesisTest130.v
index 6454bfbf1..15485499b 100644
--- a/src/Specific/ArithmeticSynthesisTest130.v
+++ b/src/Specific/ArithmeticSynthesisTest130.v
@@ -115,7 +115,7 @@ Section Ops51.
                  let eval := Positional.Fdecode (m:=m) wt in
                  eval (add a b) = (eval a  + eval b)%F }.
   Proof.
-    eexists; cbv beta zeta; intros.
+    eexists; cbv beta zeta; intros a b.
     pose proof wt_nonzero.
     let x := constr:(
         Positional.add_cps (n := sz) wt a b id) in
@@ -128,7 +128,7 @@ Section Ops51.
                  let eval := Positional.Fdecode (m:=m) wt in
                  eval (sub a b) = (eval a - eval b)%F}.
   Proof.
-    eexists; cbv beta zeta; intros.
+    eexists; cbv beta zeta; intros a b.
     pose proof wt_nonzero.
     let x := constr:(
          Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in
@@ -141,7 +141,7 @@ Section Ops51.
                  let eval := Positional.Fdecode (m := m) wt in
                  eval (opp a) = F.opp (eval a)}.
   Proof.
-    eexists; cbv beta zeta; intros.
+    eexists; cbv beta zeta; intros a.
     pose proof wt_nonzero.
     let x := constr:(
          Positional.opp_cps (n:=sz) (coef := coef) wt a id) in
@@ -154,7 +154,7 @@ Section Ops51.
                  let eval := Positional.Fdecode (m := m) wt in
                  eval (mul a b) = (eval a  * eval b)%F}.
   Proof.
-    eexists; cbv beta zeta; intros.
+    eexists; cbv beta zeta; intros a b.
     pose proof wt_nonzero.
     let x := constr:(
          Positional.mul_cps (n:=sz) (m:=sz2) wt a b
@@ -176,7 +176,7 @@ Section Ops51.
                  let eval := Positional.Fdecode (m := m) wt in
                  eval (carry a) = eval a}.
   Proof.
-    eexists; cbv beta zeta; intros.
+    eexists; cbv beta zeta; intros a.
     pose proof wt_nonzero. pose proof wt_divides_chain1.
     pose proof div_mod. pose proof wt_divides_chain2.
     let x := constr:(
diff --git a/src/Specific/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v
index 63cc76fc2..b9fad0e12 100644
--- a/src/Specific/IntegrationTestFreeze.v
+++ b/src/Specific/IntegrationTestFreeze.v
@@ -51,7 +51,7 @@ Section BoundedField25p5.
     | [ |- { f | forall a, ?phi (f a) = @?rhs a } ]
       => apply lift1_sig with (P:=fun a f => phi f = rhs a)
     end.
-    intros.
+    intros a.
     eexists_sig_etransitivity. all:cbv [phi].
     rewrite <- (proj2_sig freeze_sig).
     { set (freezeZ := proj1_sig freeze_sig).
diff --git a/src/Specific/IntegrationTestLadderstep.v b/src/Specific/IntegrationTestLadderstep.v
index 06cd4f808..b88370a48 100644
--- a/src/Specific/IntegrationTestLadderstep.v
+++ b/src/Specific/IntegrationTestLadderstep.v
@@ -92,7 +92,7 @@ Section BoundedField25p5.
       | forall a24 x1 Q Q', let eval := B.Positional.Fdecode wt in Tuple.map (n:=2) (Tuple.map (n:=2) eval) (xzladderstep a24 x1 Q Q') = FMxzladderstep (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') }.
   Proof.
     exists Mxzladderstep.
-    intros.
+    intros a24 x1 Q Q' eval.
     cbv [Mxzladderstep FMxzladderstep M.donnaladderstep].
     destruct Q, Q'; cbv [map map' fst snd Let_In eval].
     repeat rewrite ?(proj2_sig add_sig), ?(proj2_sig mul_sig), ?(proj2_sig square_sig), ?(proj2_sig sub_sig), ?(proj2_sig carry_sig).
diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v
index c8e3ba2b8..541dcaee8 100644
--- a/src/Specific/IntegrationTestLadderstep130.v
+++ b/src/Specific/IntegrationTestLadderstep130.v
@@ -57,7 +57,7 @@ Section BoundedField25p5.
       | forall a24 x1 Q Q', let eval := B.Positional.Fdecode wt in Tuple.map (n:=2) (Tuple.map (n:=2) eval) (xzladderstep a24 x1 Q Q') = FMxzladderstep (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') }.
   Proof.
     exists (@M.xzladderstep _ (proj1_sig add_sig) (proj1_sig sub_sig) (fun x y => proj1_sig carry_sig (proj1_sig mul_sig x y))).
-    intros.
+    intros a24 x1 Q Q' eval.
     cbv [FMxzladderstep M.xzladderstep].
     destruct Q, Q'; cbv [map map' fst snd Let_In eval].
     repeat rewrite ?(proj2_sig add_sig), ?(proj2_sig mul_sig), ?(proj2_sig sub_sig), ?(proj2_sig carry_sig).
diff --git a/src/Specific/IntegrationTestMul.v b/src/Specific/IntegrationTestMul.v
index 0cbc3966e..01d629bfb 100644
--- a/src/Specific/IntegrationTestMul.v
+++ b/src/Specific/IntegrationTestMul.v
@@ -50,7 +50,7 @@ Section BoundedField25p5.
     | [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ]
       => apply lift2_sig with (P:=fun a b f => phi f = rhs a b)
     end.
-    intros.
+    intros a b.
     eexists_sig_etransitivity. all:cbv [phi].
     rewrite <- (proj2_sig mul_sig).
     symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
diff --git a/src/Specific/IntegrationTestSquare.v b/src/Specific/IntegrationTestSquare.v
index eb91a13ff..d7d717c61 100644
--- a/src/Specific/IntegrationTestSquare.v
+++ b/src/Specific/IntegrationTestSquare.v
@@ -50,7 +50,7 @@ Section BoundedField25p5.
     | [ |- { f | forall a, ?phi (f a) = @?rhs a } ]
       => apply lift1_sig with (P:=fun a f => phi f = rhs a)
     end.
-    intros.
+    intros a.
     eexists_sig_etransitivity. all:cbv [phi].
     rewrite <- (proj2_sig square_sig).
     symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
diff --git a/src/Specific/IntegrationTestSub.v b/src/Specific/IntegrationTestSub.v
index 3eadc371d..7599c99e1 100644
--- a/src/Specific/IntegrationTestSub.v
+++ b/src/Specific/IntegrationTestSub.v
@@ -50,7 +50,7 @@ Section BoundedField25p5.
     | [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ]
       => apply lift2_sig with (P:=fun a b f => phi f = rhs a b)
     end.
-    intros.
+    intros a b.
     eexists_sig_etransitivity. all:cbv [phi].
     rewrite <- (proj2_sig sub_sig).
     symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v
index e03b2e36f..f35c4e9ea 100644
--- a/src/Util/AdditionChainExponentiation.v
+++ b/src/Util/AdditionChainExponentiation.v
@@ -39,7 +39,7 @@ Section AddChainExp.
       (Hl:Logic.eq (length acc) (length ref)),
       fold_chain id op is acc = (fold_chain 0 N.add is ref) * x.
   Proof using Type*.
-    induction is; intros; simpl @fold_chain.
+    intro x; induction is; intros acc ref H Hl; simpl @fold_chain.
     { repeat break_match; specialize (H 0%nat); rewrite ?nth_default_cons, ?nth_default_cons_S in H;
       solve [ simpl length in *; discriminate | apply H | rewrite scalarmult_0_l; reflexivity ]. }
     { repeat break_match. eapply IHis; intros; [|auto with distr_length]; [].
@@ -52,8 +52,8 @@ Section AddChainExp.
 
   Lemma fold_chain_exp x is: fold_chain id op is [x] = (fold_chain 0 N.add is [1]) * x.
   Proof using Type*.
-    eapply fold_chain_exp'; intros; trivial.
-    destruct i; try destruct i; rewrite ?nth_default_cons_S, ?nth_default_cons, ?nth_default_nil;
+    eapply fold_chain_exp'; trivial; intros i.
+    destruct i as [|i]; try destruct i; rewrite ?nth_default_cons_S, ?nth_default_cons, ?nth_default_nil;
       rewrite ?scalarmult_1_l, ?scalarmult_0_l; reflexivity.
   Qed.
 End AddChainExp.
diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v
index 41b21feb7..15782fa61 100644
--- a/src/Util/CPSUtil.v
+++ b/src/Util/CPSUtil.v
@@ -48,7 +48,7 @@ Fixpoint map_cps {A B} (g : A->B) ls
   end.
 Lemma map_cps_correct {A B} g ls: forall {T} f,
     @map_cps A B g ls T f = f (map g ls).
-Proof. induction ls; simpl; intros; rewrite ?IHls; reflexivity. Qed.
+Proof. induction ls as [|?? IHls]; simpl; intros; rewrite ?IHls; reflexivity. Qed.
 Create HintDb uncps discriminated. Hint Rewrite @map_cps_correct : uncps.
 
 Fixpoint flat_map_cps {A B} (g:A->forall {T}, (list B->T)->T) (ls : list A) {T} (f:list B->T)  :=
@@ -61,7 +61,7 @@ Lemma flat_map_cps_correct {A B} (g:A->forall {T}, (list B->T)->T) ls :
     (forall x T h, @g x T h = h (g x id)) ->
     @flat_map_cps A B g ls T f = f (List.flat_map (fun x => g x id) ls).
 Proof.
-  induction ls; intros; [reflexivity|].
+  induction ls as [|?? IHls]; intros T f H; [reflexivity|].
   simpl flat_map_cps. simpl flat_map.
   rewrite H; erewrite IHls by eassumption.
   reflexivity.
@@ -81,7 +81,7 @@ Fixpoint from_list_default'_cps {A} (d y:A) n xs:
 Lemma from_list_default'_cps_correct {A} n : forall d y l {T} f,
     @from_list_default'_cps A d y n l T f = f (Tuple.from_list_default' d y n l).
 Proof.
-  induction n; intros; simpl; [reflexivity|].
+  induction n as [|? IHn]; intros; simpl; [reflexivity|].
   break_match; subst; apply IHn.
 Qed.
 Definition from_list_default_cps {A} (d:A) n (xs:list A) :
@@ -136,7 +136,7 @@ Lemma on_tuple_cps_correct {A B} d (g:list A -> forall {T}, (list B->T)->T)
       (Hg : forall x {T} h, @g x T h = h (g x id)) : forall H,
     @on_tuple_cps A B d g n m xs T f = f (@Tuple.on_tuple A B (fun x => g x id) n m H xs).
 Proof.
-  cbv [on_tuple_cps Tuple.on_tuple]; intros.
+  cbv [on_tuple_cps Tuple.on_tuple]; intros H.
   rewrite to_list_cps_correct, Hg, from_list_default_cps_correct.
   rewrite (Tuple.from_list_default_eq _ _ _ (H _ (Tuple.length_to_list _))).
   reflexivity.
@@ -188,7 +188,7 @@ Lemma fold_right_cps2_correct {A B} g a0 l : forall {T} f,
   (forall b a T h, @g b a T h = h (@g b a A id)) ->
   @fold_right_cps2 A B g a0 l T f = f (List.fold_right (fun b a => @g b a A id) a0 l).
 Proof.
-  induction l; intros; [reflexivity|].
+  induction l as [|?? IHl]; intros T f H; [reflexivity|].
   simpl fold_right_cps2. simpl fold_right.
   rewrite H; erewrite IHl by eassumption.
   rewrite H; reflexivity.
@@ -225,7 +225,7 @@ Fixpoint fold_right_cps {A B} (g:B->A->A) (a0:A) (l:list B) {T} (f:A->T) :=
   end.
 Lemma fold_right_cps_correct {A B} g a0 l: forall {T} f,
     @fold_right_cps A B g a0 l T f = f (List.fold_right g a0 l).
-Proof. induction l; intros; simpl; rewrite ?IHl; auto. Qed.
+Proof. induction l as [|? l IHl]; intros; simpl; rewrite ?IHl; auto. Qed.
 Hint Rewrite @fold_right_cps_correct : uncps.
 
 Definition fold_right_no_starter_cps {A} g ls {T} (f:option A->T) :=
@@ -278,7 +278,7 @@ Module Tuple.
   Lemma mapi_with'_cps_correct {S A B n} : forall i f start xs T ret,
   (forall i s a R (ret:_->R), f i s a R ret = ret (f i s a _ id)) ->
   @mapi_with'_cps S A B n i f start xs T ret = ret (mapi_with' i (fun i s a => f i s a _ id) start xs).
-  Proof. induction n; intros; simpl; rewrite H, ?IHn by assumption; reflexivity. Qed.
+  Proof. induction n as [|n IHn]; intros i f start xs T ret H; simpl; rewrite H, ?IHn by assumption; reflexivity. Qed.
   Lemma mapi_with_cps_correct {S A B n} f start xs T ret
   (H:forall i s a R (ret:_->R), f i s a R ret = ret (f i s a _ id))
   : @mapi_with_cps S A B n f start xs T ret = ret (mapi_with (fun i s a => f i s a _ id) start xs).
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v
index cc144f062..e5f9cf0bd 100644
--- a/src/Util/Decidable.v
+++ b/src/Util/Decidable.v
@@ -16,8 +16,8 @@ Notation DecidableRel R := (forall x y, Decidable (R x y)).
 Global Instance hprop_eq_dec {A} `{DecidableRel (@eq A)} : IsHPropRel (@eq A) | 10.
 Proof. repeat intro; apply UIP_dec; trivial with nocore. Qed.
 
-Global Instance eq_dec_hprop {A} {x y : A} `{hp : IsHProp A} : Decidable (@eq A x y) | 5.
-Proof. left; apply hp. Qed.
+Global Instance eq_dec_hprop {A} {x y : A} {hp : IsHProp A} : Decidable (@eq A x y) | 5.
+Proof. left; auto. Qed.
 
 Ltac no_equalities_about x0 y0 :=
   lazymatch goal with
@@ -111,15 +111,16 @@ Global Instance dec_ge_Z : DecidableRel BinInt.Z.ge := ZArith_dec.Z_ge_dec.
 Global Instance dec_match_pair {A B} {P : A -> B -> Prop} {x : A * B}
        {HD : Decidable (P (fst x) (snd x))}
   : Decidable (let '(a, b) := x in P a b) | 1.
-Proof. destruct x; assumption. Defined.
+Proof. edestruct (_ : _ * _); assumption. Defined.
 
 Lemma not_not P {d:Decidable P} : not (not P) <-> P.
 Proof. destruct (dec P); intuition. Qed.
 
-Global Instance dec_ex_forall_not T (P:T->Prop) {d:Decidable (exists b, P b)} : Decidable (forall b, ~ P b).
+Global Instance dec_ex_forall_not : forall T (P:T->Prop) {d:Decidable (exists b, P b)}, Decidable (forall b, ~ P b).
 Proof.
+  intros T P d.
   destruct (dec (~ exists b, P b)) as [Hd|Hd]; [left|right];
-    [abstract eauto | abstract (rewrite not_not in Hd by eauto; destruct Hd; eauto) ].
+    [abstract eauto | let Hd := Hd in abstract (rewrite not_not in Hd by eauto; destruct Hd; eauto) ].
 Defined.
 
 Lemma eqsig_eq {T} {U} {Udec:DecidableRel (@eq U)} (f g:T->U) (x x':T) pf pf' :
diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index 456c9497a..affdb933a 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -83,8 +83,9 @@ Section gen.
     reflexivity.
   Defined.
 
-  Global Instance isiso_encode {y} : IsIso (encode y).
+  Global Instance isiso_encode : forall {y}, IsIso (encode y).
   Proof.
+    intro y.
     exists (@decode y).
     { intro H.
       unfold decode.
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v
index 430684070..56c7debf6 100644
--- a/src/Util/FixedWordSizesEquality.v
+++ b/src/Util/FixedWordSizesEquality.v
@@ -23,6 +23,7 @@ Lemma pow2_inj_helper x y : 2^x = 2^y -> x = y.
 Proof.
   destruct (NatUtil.nat_eq_dec x y) as [pf|pf]; [ intros; assumption | ].
   intro H; exfalso.
+  let pf := pf in
   abstract (apply pf; eapply NPeano.Nat.pow_inj_r; [ | eassumption ]; omega).
 Defined.
 Lemma pow2_inj_helper_refl x p : pow2_inj_helper x x p = eq_refl.
@@ -43,6 +44,7 @@ Proof.
   intros [pf H]; exists (pow2_inj_helper x y pf); subst v'.
   destruct (NatUtil.nat_eq_dec x y) as [H|H];
     [ | exfalso; clear -pf H;
+        let pf := pf in
         abstract (apply pow2_inj_helper in pf; omega) ].
   subst; rewrite pow2_inj_helper_refl; simpl.
   pose proof (NatUtil.UIP_nat_transparent _ _ pf eq_refl); subst pf.
@@ -99,7 +101,10 @@ Proof.
          | _, _
            => fun x y pf => match _ : False with end
          end;
-    try abstract (rewrite wordT_beq_hetero_type_lb_false in pf by omega; clear -pf; congruence).
+    match goal with
+    | [ pf : _ = _ |- _ ]
+      => abstract (rewrite wordT_beq_hetero_type_lb_false in pf by omega; clear -pf; congruence)
+    end.
 Defined.
 
 Lemma ZToWord_gen_wordToZ_gen : forall {sz} v, ZToWord_gen (@wordToZ_gen sz v) = v.
@@ -123,7 +128,7 @@ Qed.
 Lemma wordToZ_gen_ZToWord_gen_mod : forall {sz} w, (0 <= w)%Z -> wordToZ_gen (@ZToWord_gen sz w) = (w mod (2^Z.of_nat sz))%Z.
 Proof.
   unfold ZToWord_gen, wordToZ_gen.
-  intros.
+  intros sz w H.
   rewrite wordToN_NToWord_mod.
   rewrite N2Z.inj_mod by (destruct sz; simpl; congruence).
   rewrite Z2N.id, N2Z.inj_pow, nat_N_Z by assumption.
diff --git a/src/Util/ForLoop/InvariantFramework.v b/src/Util/ForLoop/InvariantFramework.v
index 503cfcdc3..2bff6bef9 100644
--- a/src/Util/ForLoop/InvariantFramework.v
+++ b/src/Util/ForLoop/InvariantFramework.v
@@ -16,7 +16,7 @@ Lemma repeat_function_ind {stateT} (P : nat -> stateT -> Prop)
   : P 0 (repeat_function body count st).
 Proof.
   revert dependent st; revert dependent body; revert dependent P.
-  induction count; intros; [ exact Pbefore | ].
+  induction count as [|? IHcount]; intros P body Pbody st Pbefore; [ exact Pbefore | ].
   { rewrite repeat_function_unroll1_end; apply Pbody; [ omega | ].
     apply (IHcount (fun c => P (S c))); auto with omega. }
 Qed.
diff --git a/src/Util/ForLoop/Unrolling.v b/src/Util/ForLoop/Unrolling.v
index e0518f39a..95b46e711 100644
--- a/src/Util/ForLoop/Unrolling.v
+++ b/src/Util/ForLoop/Unrolling.v
@@ -31,7 +31,7 @@ Section with_body.
     : repeat_function body (S count) st
       = body 1 (repeat_function (fun count => body (S count)) count st).
   Proof using Type.
-    revert st; induction count; [ reflexivity | ].
+    revert st; induction count as [|? IHcount]; [ reflexivity | ].
     intros; simpl in *; rewrite <- IHcount; reflexivity.
   Qed.
 
diff --git a/src/Util/HList.v b/src/Util/HList.v
index 2a135c75c..d2ea841d3 100644
--- a/src/Util/HList.v
+++ b/src/Util/HList.v
@@ -142,13 +142,14 @@ Proof.
   destruct n; [ simpl; tauto | apply fold_right_and_True_hlist' ].
 Qed.
 
-Global Instance mapt_Proper {n A F B}
-  : Proper
+Global Instance mapt_Proper
+  : forall {n A F B},
+    Proper
       ((forall_relation (fun x => pointwise_relation _ Logic.eq))
          ==> forall_relation (fun ts => Logic.eq ==> Logic.eq))
       (@mapt n A F B).
 Proof.
-  unfold forall_relation, pointwise_relation, respectful.
+  intro n; unfold forall_relation, pointwise_relation, respectful.
   repeat intro; subst; destruct n as [|n]; [ reflexivity | ].
   induction n; simpl in *; congruence.
 Qed.
diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v
index e4f9dde08..4d9365e4d 100644
--- a/src/Util/IterAssocOp.v
+++ b/src/Util/IterAssocOp.v
@@ -26,7 +26,7 @@ Section IterAssocOp.
 
   Lemma Pos_iter_op_succ : forall p a, Pos.iter_op op (Pos.succ p) a === op a (Pos.iter_op op p a).
   Proof using Type*.
-   induction p; intros; simpl; rewrite ?Algebra.Hierarchy.associative, ?IHp; reflexivity.
+   induction p as [p IHp|p IHp|]; intros; simpl; rewrite ?Algebra.Hierarchy.associative, ?IHp; reflexivity.
   Qed.
 
   Lemma N_iter_op_succ : forall n a, N_iter_op (N.succ n) a  === op a (N_iter_op n a).
@@ -36,7 +36,7 @@ Section IterAssocOp.
 
   Lemma N_iter_op_is_nat_iter_op : forall n a, N_iter_op n a === nat_iter_op (N.to_nat n) a.
   Proof using Type*.
-    induction n using N.peano_ind; intros; rewrite ?N2Nat.inj_succ, ?N_iter_op_succ, ?IHn; reflexivity.
+    induction n as [|n IHn] using N.peano_ind; intros; rewrite ?N2Nat.inj_succ, ?N_iter_op_succ, ?IHn; reflexivity.
   Qed.
 
   Context {sel:bool->T->T->T} {sel_correct:forall b x y, sel b x y = if b then y else x}.
@@ -90,7 +90,7 @@ Section IterAssocOp.
   Lemma funexp_test_and_op_index : forall a x acc y,
     fst (funexp (test_and_op a) (x, acc) y) = x - y.
   Proof using Type.
-    induction y; simpl; rewrite <- ?Minus.minus_n_O; try reflexivity.
+    induction y as [|? IHy]; simpl; rewrite <- ?Minus.minus_n_O; try reflexivity.
     match goal with |- context[funexp ?a ?b ?c] => destruct (funexp a b c) as [i acc'] end.
     simpl in IHy.
     unfold test_and_op.
@@ -129,7 +129,7 @@ Global Instance Proper_funexp {T R} {Equivalence_R:Equivalence R}
   : Proper ((R==>R) ==> R ==> Logic.eq ==> R) (@funexp T).
 Proof.
   repeat intro; subst.
-  match goal with [n0 : nat |- _ ] => rename n0 into n; induction n end; [solve [trivial]|].
+  match goal with [n0 : nat |- _ ] => rename n0 into n; induction n as [|n IHn] end; [solve [trivial]|].
   match goal with
       [H: (_ ==> _)%signature _ _ |- _ ] =>
       etransitivity; solve [eapply (H _ _ IHn)|reflexivity]
@@ -169,7 +169,8 @@ Global Instance Proper_iter_op {T R} {Equivalence_R:@Equivalence T R} :
 Proof.
   repeat match goal with
            | _ => solve [ reflexivity | congruence | eauto 99 ]
-           | _ => progress eapply (Proper_funexp (R:=(fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT))))
+           | [ R : _ |- _ ]
+             => progress eapply (Proper_funexp (R:=(fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT))))
            | _ => progress eapply Proper_test_and_op
            | _ => progress split
            | _ => progress (cbv [fst snd pointwise_relation respectful] in * )
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index b49367600..6c6f96761 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -7,6 +7,8 @@ Require Import Crypto.Util.NatUtil.
 Require Export Crypto.Util.FixCoqMistakes.
 Require Export Crypto.Util.Tactics.BreakMatch.
 Require Export Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.RewriteHyp.
 
 Create HintDb distr_length discriminated.
 Create HintDb simpl_set_nth discriminated.
@@ -77,7 +79,7 @@ Module Export List.
   Lemma in_seq len start n :
     In n (seq start len) <-> start <= n < start+len.
   Proof.
-   revert start. induction len; simpl; intros.
+   revert start. induction len as [|len IHlen]; simpl; intros.
    - rewrite <- plus_n_O. split;[easy|].
      intros (H,H'). apply (Lt.lt_irrefl _ (Lt.le_lt_trans _ _ _ H H')).
    - rewrite IHlen, <- plus_n_Sm; simpl; split.
@@ -136,7 +138,7 @@ Module Export List.
 
     Lemma firstn_all2 n: forall (l:list A), (length l) <= n -> firstn n l = l.
     Proof using Type. induction n as [|k iHk].
-           - intro. inversion 1 as [H1|?].
+           - intro l. inversion 1 as [H1|?].
              rewrite (length_zero_iff_nil l) in H1. subst. now simpl.
            - destruct l as [|x xs]; simpl.
              * now reflexivity.
@@ -157,7 +159,7 @@ Module Export List.
           n <= length l -> length (firstn n l) = n.
     Proof using Type. induction l as [|x xs Hrec].
            - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl.
-           - destruct n.
+           - destruct n as [|n].
              * now simpl.
              * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H).
     Qed.
@@ -318,26 +320,26 @@ Lemma nth_error_seq : forall i start len,
   if lt_dec i len
   then Some (start + i)
   else None.
-  induction i; destruct len; nth_tac'; erewrite IHi; nth_tac'.
+  induction i as [|? IHi]; destruct len; nth_tac'; erewrite IHi; nth_tac'.
 Qed.
 
 Lemma nth_error_error_length : forall A i (xs:list A), nth_error xs i = None ->
   i >= length xs.
 Proof.
-  induction i; destruct xs; nth_tac'; try specialize (IHi _ H); omega.
+  induction i as [|? IHi]; destruct xs; nth_tac'; try match goal with H : _ |- _ => specialize (IHi _ H) end; omega.
 Qed.
 
 Lemma nth_error_value_length : forall A i (xs:list A) x, nth_error xs i = Some x ->
   i < length xs.
 Proof.
-  induction i; destruct xs; nth_tac'; try specialize (IHi _ _ H); omega.
+  induction i as [|? IHi]; destruct xs; nth_tac'; try match goal with H : _ |- _ => specialize (IHi _ _ H) end; omega.
 Qed.
 
 Lemma nth_error_length_error : forall A i (xs:list A),
   i >= length xs ->
   nth_error xs i = None.
 Proof.
-  induction i; destruct xs; nth_tac'; rewrite IHi by omega; auto.
+  induction i as [|? IHi]; destruct xs; nth_tac'; rewrite IHi by omega; auto.
 Qed.
 Hint Resolve nth_error_length_error.
 Hint Rewrite @nth_error_length_error using omega : simpl_nth_error.
@@ -345,11 +347,12 @@ Hint Rewrite @nth_error_length_error using omega : simpl_nth_error.
 Lemma map_nth_default : forall (A B : Type) (f : A -> B) n x y l,
   (n < length l) -> nth_default y (map f l) n = f (nth_default x l n).
 Proof.
-  intros.
+  intros A B f n x y l H.
   unfold nth_default.
   erewrite map_nth_error.
   reflexivity.
   nth_tac'.
+  let H0 := match goal with H0 : _ = None |- _ => H0 end in
   pose proof (nth_error_error_length A n l H0).
   omega.
 Qed.
@@ -362,7 +365,7 @@ Proof. reflexivity. Qed.
 Lemma In_nth : forall {A} (x : A) d xs, In x xs ->
   exists i, i < length xs /\ nth i xs d = x.
 Proof.
-  induction xs; intros;
+  induction xs as [|?? IHxs]; intros;
     match goal with H : In _ _ |- _ => simpl in H; destruct H end.
   + subst. exists 0. simpl; split; auto || omega.
   + destruct IHxs as [i [ ]]; auto.
@@ -423,7 +426,7 @@ Lemma update_nth_ext {T} f g n
   : forall xs, (forall x, nth_error xs n = Some x -> f x = g x)
                -> @update_nth T n f xs = @update_nth T n g xs.
 Proof.
-  induction n; destruct xs; simpl; intros H;
+  induction n as [|n IHn]; destruct xs; simpl; intros H;
     try rewrite IHn; try rewrite H;
       try congruence; trivial.
 Qed.
@@ -436,7 +439,7 @@ Lemma update_nth_id_eq_specific {T} f n
   : forall (xs : list T) (H : forall x, nth_error xs n = Some x -> f x = x),
     update_nth n f xs = xs.
 Proof.
-  induction n; destruct xs; simpl; intros;
+  induction n as [|n IHn]; destruct xs; simpl; intros H;
     try rewrite IHn; try rewrite H; unfold value in *;
       try congruence; assumption.
 Qed.
@@ -461,7 +464,7 @@ Lemma nth_update_nth : forall m {T} (xs:list T) (n:nat) (f:T -> T),
   then option_map f (nth_error xs n)
   else nth_error xs n.
 Proof.
-  induction m.
+  induction m as [|? IHm].
   { destruct n, xs; auto. }
   { destruct xs, n; intros; simpl; auto;
       [ | rewrite IHm ]; clear IHm;
@@ -499,7 +502,7 @@ Lemma nth_set_nth : forall m {T} (xs:list T) (n:nat) x,
   then (if lt_dec n (length xs) then Some x else None)
   else nth_error xs n.
 Proof.
-  intros; unfold set_nth; rewrite nth_update_nth.
+  intros m T xs n x; unfold set_nth; rewrite nth_update_nth.
   destruct (nth_error xs n) eqn:?, (lt_dec n (length xs)) as [p|p];
     rewrite <- nth_error_Some in p;
     solve [ reflexivity
@@ -522,7 +525,7 @@ Qed.
 Lemma nth_error_length_not_error : forall {A} (i : nat) (xs : list A),
   nth_error xs i = None -> (i < length xs)%nat -> False.
 Proof.
-  intros.
+  intros A i xs H H0.
   destruct (nth_error_length_exists_value i xs); intuition; congruence.
 Qed.
 
@@ -540,7 +543,7 @@ Proof. auto. Qed.
 Lemma destruct_repeat : forall {A} xs y, (forall x : A, In x xs -> x = y) ->
   xs = nil \/ exists xs', xs = y :: xs' /\ (forall x : A, In x xs' -> x = y).
 Proof.
-  destruct xs; intros; try tauto.
+  destruct xs as [|? xs]; intros; try tauto.
   right.
   exists xs; split.
   + f_equal; auto using in_eq.
@@ -590,7 +593,7 @@ Lemma update_nth_equiv_splice_nth: forall {T} n f (xs:list T),
        end
   else xs.
 Proof.
-  induction n; destruct xs; intros;
+  induction n as [|? IHn]; destruct xs; intros;
     autorewrite with simpl_update_nth simpl_nth_default in *; simpl in *;
       try (erewrite IHn; clear IHn); auto.
   repeat break_match; remove_nth_error; try reflexivity; try omega.
@@ -601,17 +604,17 @@ Lemma splice_nth_equiv_set_nth : forall {T} n x (xs:list T),
   if lt_dec n (length xs)
   then set_nth n x xs
   else xs ++ x::nil.
-Proof. intros; rewrite splice_nth_equiv_update_nth with (f := fun _ => x); auto. Qed.
+Proof. intros T n x xs; rewrite splice_nth_equiv_update_nth with (f := fun _ => x); auto. Qed.
 
 Lemma splice_nth_equiv_set_nth_set : forall {T} n x (xs:list T),
   n < length xs ->
   splice_nth n x xs = set_nth n x xs.
-Proof. intros; rewrite splice_nth_equiv_update_nth_update with (f := fun _ => x); auto. Qed.
+Proof. intros T n x xs H; rewrite splice_nth_equiv_update_nth_update with (f := fun _ => x); auto. Qed.
 
 Lemma splice_nth_equiv_set_nth_snoc : forall {T} n x (xs:list T),
   n >= length xs ->
   splice_nth n x xs = xs ++ x::nil.
-Proof. intros; rewrite splice_nth_equiv_update_nth_snoc with (f := fun _ => x); auto. Qed.
+Proof. intros T n x xs H; rewrite splice_nth_equiv_update_nth_snoc with (f := fun _ => x); auto. Qed.
 
 Lemma set_nth_equiv_splice_nth: forall {T} n x (xs:list T),
   set_nth n x xs =
@@ -619,7 +622,7 @@ Lemma set_nth_equiv_splice_nth: forall {T} n x (xs:list T),
   then splice_nth n x xs
   else xs.
 Proof.
-  intros; unfold set_nth; rewrite update_nth_equiv_splice_nth with (f := fun _ => x); auto.
+  intros T n x xs; unfold set_nth; rewrite update_nth_equiv_splice_nth with (f := fun _ => x); auto.
   repeat break_match; remove_nth_error; trivial.
 Qed.
 
@@ -627,7 +630,7 @@ Lemma combine_update_nth : forall {A B} n f g (xs:list A) (ys:list B),
   combine (update_nth n f xs) (update_nth n g ys) =
   update_nth n (fun xy => (f (fst xy), g (snd xy))) (combine xs ys).
 Proof.
-  induction n; destruct xs, ys; simpl; try rewrite IHn; reflexivity.
+  induction n as [|? IHn]; destruct xs, ys; simpl; try rewrite IHn; reflexivity.
 Qed.
 
 (* grumble, grumble, [rewrite] is bad at inferring the identity function, and constant functions *)
@@ -669,7 +672,7 @@ Lemma combine_set_nth : forall {A B} n (x:A) xs (ys:list B),
     | Some y => set_nth n (x,y) (combine xs ys)
     end.
 Proof.
-  intros; unfold set_nth; rewrite combine_update_nth_l.
+  intros A B n x xs ys; unfold set_nth; rewrite combine_update_nth_l.
   nth_tac;
     [ repeat rewrite_rev_combine_update_nth; apply f_equal2
     | assert (nth_error (combine xs ys) n = None)
@@ -686,15 +689,15 @@ Qed.
 Lemma In_nth_error_value : forall {T} xs (x:T),
   In x xs -> exists n, nth_error xs n = Some x.
 Proof.
-  induction xs; nth_tac; destruct_head or; subst.
+  induction xs as [|?? IHxs]; nth_tac; destruct_head or; subst.
   - exists 0; reflexivity.
-  - edestruct IHxs; eauto. exists (S x0). eauto.
+  - edestruct IHxs as [x0]; eauto. exists (S x0). eauto.
 Qed.
 
 Lemma nth_value_index : forall {T} i xs (x:T),
   nth_error xs i = Some x -> In i (seq 0 (length xs)).
 Proof.
-  induction i; destruct xs; nth_tac; right.
+  induction i as [|? IHi]; destruct xs; nth_tac; right.
   rewrite <- seq_shift; apply in_map; eapply IHi; eauto.
 Qed.
 
@@ -703,7 +706,7 @@ Lemma nth_error_app : forall {T} n (xs ys:list T), nth_error (xs ++ ys) n =
   then nth_error xs n
   else nth_error ys (n - length xs).
 Proof.
-  induction n; destruct xs; nth_tac;
+  induction n as [|n IHn]; destruct xs as [|? xs]; nth_tac;
     rewrite IHn; destruct (lt_dec n (length xs)); trivial; omega.
 Qed.
 
@@ -712,7 +715,7 @@ Lemma nth_default_app : forall {T} n x (xs ys:list T), nth_default x (xs ++ ys)
   then nth_default x xs n
   else nth_default x ys (n - length xs).
 Proof.
-  intros.
+  intros T n x xs ys.
   unfold nth_default.
   rewrite nth_error_app.
   destruct (lt_dec n (length xs)); auto.
@@ -952,7 +955,7 @@ Lemma list012 : forall {T} (xs:list T),
   \/ (exists x, xs = x::nil)
   \/ (exists x xs' y, xs = x::xs'++y::nil).
 Proof.
-  destruct xs; auto.
+  destruct xs as [|? xs]; auto.
   right.
   destruct xs using rev_ind. {
     left; eexists; auto.
@@ -1017,7 +1020,7 @@ Hint Rewrite @set_nth_nil : simpl_set_nth.
 Lemma skipn_nth_default : forall {T} n us (d : T), (n < length us)%nat ->
  skipn n us = nth_default d us n :: skipn (S n) us.
 Proof.
-  induction n; destruct us; intros; nth_tac.
+  induction n as [|n IHn]; destruct us as [|? us]; intros d H; nth_tac.
   rewrite (IHn us d) at 1 by omega.
   nth_tac.
 Qed.
@@ -1025,10 +1028,13 @@ Qed.
 Lemma nth_default_out_of_bounds : forall {T} n us (d : T), (n >= length us)%nat ->
   nth_default d us n = d.
 Proof.
-  induction n; unfold nth_default; nth_tac; destruct us; nth_tac.
+  induction n as [|n IHn]; unfold nth_default; nth_tac;
+    let us' := match goal with us : list _ |- _ => us end in
+    destruct us' as [|? us]; nth_tac.
   assert (n >= length us)%nat by omega.
-  pose proof (nth_error_length_error _ n us H1).
-  rewrite H0 in H2.
+  pose proof (nth_error_length_error _ n us).
+  specialize_by_assumption.
+  rewrite_hyp * in *.
   congruence.
 Qed.
 
@@ -1131,12 +1137,12 @@ Hint Rewrite @map_nth_default_always : push_nth_default.
 
 Lemma map_S_seq {A} (f:nat->A) len : forall start,
   List.map (fun i => f (S i)) (seq start len) = List.map f (seq (S start) len).
-Proof. induction len; intros; simpl; rewrite ?IHlen; reflexivity. Qed.
+Proof. induction len as [|len IHlen]; intros; simpl; rewrite ?IHlen; reflexivity. Qed.
 
 Lemma fold_right_and_True_forall_In_iff : forall {T} (l : list T) (P : T -> Prop),
   (forall x, In x l -> P x) <-> fold_right and True (map P l).
 Proof.
-  induction l; intros; simpl; try tauto.
+  induction l as [|?? IHl]; intros; simpl; try tauto.
   rewrite <- IHl.
   intuition (subst; auto).
 Qed.
@@ -1145,7 +1151,7 @@ Lemma fold_right_invariant : forall {A B} P (f: A -> B -> B) l x,
   P x -> (forall y, In y l -> forall z, P z -> P (f y z)) ->
   P (fold_right f x l).
 Proof.
-  induction l; intros ? ? step; auto.
+  induction l as [|a l IHl]; intros ? ? step; auto.
   simpl.
   apply step; try apply in_eq.
   apply IHl; auto.
@@ -1167,7 +1173,7 @@ Qed.
 Lemma In_firstn_skipn_split {T} n (x : T)
   : forall l, In x l <-> In x (firstn n l) \/ In x (skipn n l).
 Proof.
-  split; revert l; induction n; destruct l; boring.
+  intro l; split; revert l; induction n; destruct l; boring.
   match goal with
   | [ IH : forall l, In ?x l -> _ \/ _, H' : In ?x ?ls |- _ ]
     => destruct (IH _ H')
@@ -1177,7 +1183,7 @@ Qed.
 Lemma firstn_firstn_min : forall {A} m n (l : list A),
     firstn n (firstn m l) = firstn (min n m) l.
 Proof.
-  induction m; destruct n; intros; try omega; auto.
+  induction m as [|? IHm]; destruct n; intros l; try omega; auto.
   destruct l; auto.
   simpl.
   f_equal.
@@ -1187,7 +1193,7 @@ Qed.
 Lemma firstn_firstn : forall {A} m n (l : list A), (n <= m)%nat ->
   firstn n (firstn m l) = firstn n l.
 Proof.
-  intros; rewrite firstn_firstn_min.
+  intros A m n l H; rewrite firstn_firstn_min.
   apply Min.min_case_strong; intro; [ reflexivity | ].
   assert (n = m) by omega; subst; reflexivity.
 Qed.
@@ -1197,7 +1203,7 @@ Hint Rewrite @firstn_firstn using omega : push_firstn.
 Lemma firstn_succ : forall {A} (d : A) n l, (n < length l)%nat ->
   firstn (S n) l = (firstn n l) ++ nth_default d l n :: nil.
 Proof.
-  induction n; destruct l; rewrite ?(@nil_length0 A); intros; try omega.
+  intros A d; induction n as [|? IHn]; destruct l; rewrite ?(@nil_length0 A); intros; try omega.
   + rewrite nth_default_cons; auto.
   + simpl.
     rewrite nth_default_cons_S.
@@ -1208,20 +1214,20 @@ Qed.
 Lemma firstn_seq k a b
   : firstn k (seq a b) = seq a (min k b).
 Proof.
-  revert k a; induction b, k; simpl; try reflexivity.
+  revert k a; induction b as [|? IHb], k; simpl; try reflexivity.
   intros; rewrite IHb; reflexivity.
 Qed.
 
 Lemma skipn_seq k a b
   : skipn k (seq a b) = seq (k + a) (b - k).
 Proof.
-  revert k a; induction b, k; simpl; try reflexivity.
+  revert k a; induction b as [|? IHb], k; simpl; try reflexivity.
   intros; rewrite IHb; simpl; f_equal; omega.
 Qed.
 
 Lemma update_nth_out_of_bounds : forall {A} n f xs, n >= length xs -> @update_nth A n f xs = xs.
 Proof.
-  induction n; destruct xs; simpl; try congruence; try omega; intros.
+  induction n as [|n IHn]; destruct xs; simpl; try congruence; try omega; intros.
   rewrite IHn by omega; reflexivity.
 Qed.
 
@@ -1235,8 +1241,8 @@ Lemma update_nth_nth_default_full : forall {A} (d:A) n f l i,
     else nth_default d l i
   else d.
 Proof.
-  induction n; (destruct l; simpl in *; [ intros; destruct i; simpl; try reflexivity; omega | ]);
-    intros; repeat break_match; subst; try destruct i;
+  induction n as [|n IHn]; (destruct l; simpl in *; [ intros i **; destruct i; simpl; try reflexivity; omega | ]);
+    intros i **; repeat break_match; subst; try destruct i;
       repeat first [ progress break_match
                    | progress subst
                    | progress boring
@@ -1273,7 +1279,7 @@ Hint Rewrite @set_nth_nth_default using (omega || distr_length; omega) : push_nt
 Lemma nth_default_preserves_properties : forall {A} (P : A -> Prop) l n d,
   (forall x, In x l -> P x) -> P d -> P (nth_default d l n).
 Proof.
-  intros; rewrite nth_default_eq.
+  intros A P l n d H H0; rewrite nth_default_eq.
   destruct (nth_in_or_default n l d); auto.
   congruence.
 Qed.
@@ -1282,7 +1288,7 @@ Lemma nth_default_preserves_properties_length_dep :
   forall {A} (P : A -> Prop) l n d,
   (forall x, In x l -> n < (length l) -> P x) -> ((~ n < length l) -> P d) -> P (nth_default d l n).
 Proof.
-  intros.
+  intros A P l n d H H0.
   destruct (lt_dec n (length l)).
   + rewrite nth_default_eq; auto using nth_In.
   + rewrite nth_default_out_of_bounds by omega.
@@ -1300,7 +1306,7 @@ Qed.
 Lemma nth_error_exists_first : forall {T} l (x : T) (H : nth_error l 0 = Some x),
   exists l', l = x :: l'.
 Proof.
-  induction l; try discriminate; eexists.
+  induction l; try discriminate; intros x H; eexists.
   apply nth_error_first in H.
   subst; eauto.
 Qed.
@@ -1308,7 +1314,7 @@ Qed.
 Lemma list_elementwise_eq : forall {T} (l1 l2 : list T),
   (forall i, nth_error l1 i = nth_error l2 i) -> l1 = l2.
 Proof.
-  induction l1, l2; intros; try reflexivity;
+  induction l1, l2; intros H; try reflexivity;
     pose proof (H 0%nat) as Hfirst; simpl in Hfirst; inversion Hfirst.
   f_equal.
   apply IHl1.
@@ -1337,7 +1343,7 @@ Hint Rewrite @sum_firstn_all using omega : simpl_sum_firstn.
 Lemma sum_firstn_succ_default : forall l i,
   sum_firstn l (S i) = (nth_default 0 l i + sum_firstn l i)%Z.
 Proof.
-  unfold sum_firstn; induction l, i;
+  unfold sum_firstn; induction l as [|a l IHl], i;
     intros; autorewrite with simpl_nth_default simpl_firstn simpl_fold_right in *;
       try reflexivity.
   rewrite IHl; omega.
@@ -1404,7 +1410,7 @@ Hint Resolve sum_firstn_nonnegative : znonzero.
 Lemma sum_firstn_app : forall xs ys n,
   sum_firstn (xs ++ ys) n = (sum_firstn xs n + sum_firstn ys (n - length xs))%Z.
 Proof.
-  induction xs; simpl.
+  induction xs as [|a xs IHxs]; simpl.
   { intros ys n; autorewrite with simpl_sum_firstn; simpl.
     f_equal; omega. }
   { intros ys [|n]; autorewrite with simpl_sum_firstn; simpl; [ reflexivity | ].
@@ -1428,7 +1434,7 @@ Proof. reflexivity. Qed.
 Lemma nth_error_skipn : forall {A} n (l : list A) m,
 nth_error (skipn n l) m = nth_error l (n + m).
 Proof.
-induction n; destruct l; boring.
+induction n as [|n IHn]; destruct l; boring.
 apply nth_error_nil_error.
 Qed.
 Hint Rewrite @nth_error_skipn : push_nth_error.
@@ -1454,7 +1460,7 @@ Qed.
 Lemma sum_firstn_prefix_le' : forall l n m, (forall x, In x l -> (0 <= x)%Z) ->
                                             (sum_firstn l n <= sum_firstn l (n + m))%Z.
 Proof.
-intros.
+intros l n m H.
 rewrite sum_firstn_skipn.
 pose proof (sum_firstn_nonnegative m (skipn n l)) as Hskipn_nonneg.
 match type of Hskipn_nonneg with
@@ -1468,7 +1474,7 @@ Lemma sum_firstn_prefix_le : forall l n m, (forall x, In x l -> (0 <= x)%Z) ->
                                             (n <= m)%nat ->
                                             (sum_firstn l n <= sum_firstn l m)%Z.
 Proof.
-intros.
+intros l n m H H0.
 replace m with (n + (m - n))%nat by omega.
 auto using sum_firstn_prefix_le'.
 Qed.
@@ -1478,17 +1484,17 @@ Lemma sum_firstn_pos_lt_succ : forall l n m, (forall x, In x l -> (0 <= x)%Z) ->
                                         (sum_firstn l n < sum_firstn l (S m))%Z ->
                                         (n <= m)%nat.
 Proof.
-intros.
+intros l n m H H0 H1.
 destruct (le_dec n m); auto.
 replace n with (m + (n - m))%nat in H1 by omega.
 rewrite sum_firstn_skipn in H1.
 rewrite sum_firstn_succ_default in *.
-match goal with H : (?a + ?b < ?c + ?a)%Z |- _ => assert (b < c)%Z by omega end.
+match goal with H : (?a + ?b < ?c + ?a)%Z |- _ => assert (H2 : (b < c)%Z) by omega end.
 destruct (lt_dec m (length l)). {
     rewrite skipn_nth_default with (d := 0%Z) in H2 by assumption.
     replace (n - m)%nat with (S (n - S m))%nat in H2 by omega.
     rewrite sum_firstn_succ_cons in H2.
-    pose proof (sum_firstn_nonnegative (n - S m) (skipn (S m) l)).
+    pose proof (sum_firstn_nonnegative (n - S m) (skipn (S m) l)) as H3.
     match type of H3 with
       ?P -> _ => assert P as Q; [ | specialize (H3 Q); omega ] end.
     intros ? A.
@@ -1522,7 +1528,7 @@ Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2,
     then f (nth_default d1 ls1 i) (nth_default d2 ls2 i)
     else d.
 Proof.
-  induction ls1, ls2.
+  induction ls1 as [|a ls1 IHls1], ls2.
   + cbv [map2 length min].
     intros.
     break_match; try omega.
@@ -1539,7 +1545,7 @@ Proof.
     destruct i.
     - intros. rewrite !nth_default_cons.
       break_match; auto; omega.
-    - intros. rewrite !nth_default_cons_S.
+    - intros d d1 d2. rewrite !nth_default_cons_S.
       rewrite IHls1 with (d1 := d1) (d2 := d2).
       repeat break_match; auto; omega.
 Qed.
@@ -1576,7 +1582,7 @@ Section OpaqueMap2.
   Lemma map2_length : forall A B C (f : A -> B -> C) ls1 ls2,
       length (map2 f ls1 ls2) = min (length ls1) (length ls2).
   Proof.
-    induction ls1, ls2; intros; try solve [cbv; auto].
+    induction ls1 as [|a ls1 IHls1], ls2; intros; try solve [cbv; auto].
     rewrite map2_cons, !length_cons, IHls1.
     auto.
   Qed.
@@ -1587,7 +1593,7 @@ Section OpaqueMap2.
       (length ls1 = length ls2) ->
       map2 f (ls1 ++ ls1') (ls2 ++ ls2') = map2 f ls1 ls2 ++ map2 f ls1' ls2'.
   Proof.
-    induction ls1, ls2; intros; rewrite ?map2_nil_r, ?app_nil_l; try congruence;
+    induction ls1 as [|a ls1 IHls1], ls2; intros; rewrite ?map2_nil_r, ?app_nil_l; try congruence;
       simpl_list_lengths; try omega.
     rewrite <-!app_comm_cons, !map2_cons.
     rewrite IHls1; auto.
@@ -1611,15 +1617,15 @@ Require Import Coq.Lists.SetoidList.
 Global Instance Proper_nth_default : forall A eq,
   Proper (eq==>eqlistA eq==>Logic.eq==>eq) (nth_default (A:=A)).
 Proof.
-  do 5 intro; subst; induction 1.
+  intros A ee x y H; subst; induction 1.
   + repeat intro; rewrite !nth_default_nil; assumption.
-  + repeat intro; subst; destruct y0; rewrite ?nth_default_cons, ?nth_default_cons_S; auto.
+  + intros x1 y0 H2; subst; destruct y0; rewrite ?nth_default_cons, ?nth_default_cons_S; auto.
 Qed.
 
 Lemma fold_right_andb_true_map_iff A (ls : list A) f
   : List.fold_right andb true (List.map f ls) = true <-> forall i, List.In i ls -> f i = true.
 Proof.
-  induction ls; simpl; [ | rewrite Bool.andb_true_iff, IHls ]; try tauto.
+  induction ls as [|a ls IHls]; simpl; [ | rewrite Bool.andb_true_iff, IHls ]; try tauto.
   intuition (congruence || eauto).
 Qed.
 
@@ -1633,16 +1639,17 @@ Qed.
 Lemma Forall2_forall_iff : forall {A} R (xs ys : list A) d, length xs = length ys ->
   (Forall2 R xs ys <-> (forall i, (i < length xs)%nat -> R (nth_default d xs i) (nth_default d ys i))).
 Proof.
-  split; intros.
+  intros A R xs ys d H; split; [ intros H0 i H1 | intros H0 ].
+
   + revert xs ys H H0 H1.
-    induction i; intros; destruct H0; distr_length; autorewrite with push_nth_default; auto.
+    induction i as [|i IHi]; intros xs ys H H0 H1; destruct H0; distr_length; autorewrite with push_nth_default; auto.
     eapply IHi; auto. omega.
-  + revert xs ys H H0; induction xs; intros; destruct ys; distr_length; econstructor.
+  + revert xs ys H H0; induction xs as [|a xs IHxs]; intros ys H H0; destruct ys; distr_length; econstructor.
     - specialize (H0 0%nat).
       autorewrite with push_nth_default in *; auto.
       apply H0; omega.
     - apply IHxs; try omega.
-      intros.
+      intros i H1.
       specialize (H0 (S i)).
       autorewrite with push_nth_default in *; auto.
       apply H0; omega.
@@ -1653,7 +1660,7 @@ Lemma nth_default_firstn : forall {A} (d : A) l i n,
                                  then if lt_dec i n then nth_default d l i else d
                                  else nth_default d l i.
 Proof.
-  induction n; intros; break_match; autorewrite with push_nth_default; auto; try omega.
+  intros A d l i; induction n as [|n IHn]; break_match; autorewrite with push_nth_default; auto; try omega.
   + rewrite (firstn_succ d) by omega.
     autorewrite with push_nth_default; repeat (break_match_hyps; break_match; distr_length);
       rewrite Min.min_l in * by omega; try omega.
@@ -1677,8 +1684,8 @@ Hint Rewrite repeat_length : distr_length.
 Lemma repeat_spec_iff : forall {A} (ls : list A) x n,
     (length ls = n /\ forall y, In y ls -> y = x) <-> ls = repeat x n.
 Proof.
-  split; [ revert A ls x n | intro; subst; eauto using repeat_length, repeat_spec ].
-  induction ls, n; simpl; intros; intuition try congruence.
+  intros A ls x n; split; [ revert A ls x n | intro; subst; eauto using repeat_length, repeat_spec ].
+  induction ls as [|a ls IHls], n; simpl; intros; intuition try congruence.
   f_equal; auto.
 Qed.
 
@@ -1714,13 +1721,13 @@ Qed.
 Lemma pointwise_map {A B} : Proper ((pointwise_relation _ eq) ==> eq ==> eq) (@List.map A B).
 Proof.
   repeat intro; cbv [pointwise_relation] in *; subst.
-  match goal with [H:list _ |- _ ] => induction H as [|? IH] end; [reflexivity|].
+  match goal with [H:list _ |- _ ] => induction H as [|? IH IHIH] end; [reflexivity|].
   simpl. rewrite IHIH. congruence.
 Qed.
 
 Lemma map_map2 {A B C D} (f:A -> B -> C) (g:C -> D) (xs:list A) (ys:list B) : List.map g (map2 f xs ys) = map2 (fun (a : A) (b : B) => g (f a b)) xs ys.
 Proof.
-  revert ys; induction xs; intros; [reflexivity|].
+  revert ys; induction xs as [|a xs IHxs]; intros ys; [reflexivity|].
   destruct ys; [reflexivity|].
   simpl. rewrite IHxs. reflexivity.
 Qed.
@@ -1728,7 +1735,7 @@ Qed.
 Lemma map2_fst {A B C} (f:A -> C) (xs:list A) : forall (ys:list B), length xs = length ys ->
   map2 (fun (a : A) (_ : B) => f a) xs ys = List.map f xs.
 Proof.
-  induction xs; intros; [reflexivity|].
+  induction xs as [|a xs IHxs]; intros ys **; [reflexivity|].
   destruct ys; [simpl in *; discriminate|].
   simpl. rewrite IHxs by eauto. reflexivity.
 Qed.
@@ -1736,7 +1743,7 @@ Qed.
 Lemma map2_flip {A B C} (f:A -> B -> C) (xs:list A) : forall (ys: list B),
    map2 (fun b a => f a b) ys xs = map2 f xs ys.
 Proof.
-  induction xs; destruct ys; try reflexivity; [].
+  induction xs as [|a xs IHxs]; destruct ys; try reflexivity; [].
   simpl. rewrite IHxs. reflexivity.
 Qed.
 
@@ -1747,6 +1754,6 @@ Proof. intros. rewrite map2_flip. eauto using map2_fst. Qed.
 Lemma map2_map {A B C A' B'} (f:A -> B -> C) (g:A' -> A) (h:B' -> B) (xs:list A') (ys:list B')
   : map2 f (List.map g xs) (List.map h ys) = map2 (fun a b => f (g a) (h b)) xs ys.
 Proof.
-  revert ys; induction xs; destruct ys; intros; try reflexivity; [].
+  revert ys; induction xs as [|a xs IHxs]; destruct ys; intros; try reflexivity; [].
   simpl. rewrite IHxs. reflexivity.
 Qed.
diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v
index d76be63aa..9321f2b23 100644
--- a/src/Util/NUtil.v
+++ b/src/Util/NUtil.v
@@ -26,7 +26,7 @@ Module N.
 
   Lemma size_nat_equiv : forall n, N.size_nat n = N.to_nat (N.size n).
   Proof.
-    destruct n; auto; simpl; induction p; simpl; auto; rewrite IHp, Pnat.Pos2Nat.inj_succ; reflexivity.
+    destruct n as [|p]; auto; simpl; induction p as [p IHp|p IHp|]; simpl; auto; rewrite IHp, Pnat.Pos2Nat.inj_succ; reflexivity.
   Qed.
 
   Lemma size_nat_le a b : (a <= b)%N -> (N.size_nat a <= N.size_nat b)%nat.
@@ -39,7 +39,7 @@ Module N.
   Lemma shiftr_size : forall n bound, N.size_nat n <= bound ->
     N.shiftr_nat n bound = 0%N.
   Proof.
-    intros.
+    intros n bound H.
     rewrite <- (Nat2N.id bound).
     rewrite Nshiftr_nat_equiv.
     destruct (N.eq_dec n 0); subst; [apply N.shiftr_0_l|].
@@ -86,7 +86,7 @@ Module N.
     then S (2 * N.to_nat (N.shiftr_nat n (S i)))
     else (2 * N.to_nat (N.shiftr_nat n (S i))).
   Proof.
-    intros.
+    intros n i.
     rewrite Nshiftr_nat_S.
     case_eq (N.testbit_nat n i); intro testbit_i;
       pose proof (Nshiftr_nat_spec n i 0) as shiftr_n_odd;
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 99d0be29c..80169c784 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -105,8 +105,8 @@ Ltac nat_beq_to_eq :=
 
 Lemma div_minus : forall a b, b <> 0 -> (a + b) / b = a / b + 1.
 Proof.
-  intros.
-  assert (b = 1 * b) by omega.
+  intros a b H.
+  assert (H0 : b = 1 * b) by omega.
   rewrite H0 at 1.
   rewrite <- Nat.div_add by auto.
   reflexivity.
@@ -114,7 +114,7 @@ Qed.
 
 Lemma pred_mod : forall m, (0 < m)%nat -> ((pred m) mod m)%nat = pred m.
 Proof.
-  intros; apply Nat.mod_small.
+  intros m H; apply Nat.mod_small.
   destruct m; try omega; rewrite Nat.pred_succ; auto.
 Qed.
 
@@ -141,7 +141,7 @@ Qed.
 Lemma divide2_1mod4_nat : forall c x, c = x / 4 -> x mod 4 = 1 -> exists y, 2 * y = (x / 2).
 Proof.
   assert (4 <> 0) as ne40 by omega.
-  induction c; intros; pose proof (div_mod x 4 ne40); rewrite <- H in H1. {
+  induction c; intros x H H0; pose proof (div_mod x 4 ne40) as H1; rewrite <- H in H1. {
     rewrite H0 in H1.
     simpl in H1.
     rewrite H1.
@@ -155,8 +155,8 @@ Proof.
     apply Nat.add_cancel_r in H.
     replace x with ((x - 4) + (1 * 4)) in H0 by omega.
     rewrite Nat.mod_add in H0 by auto.
-    pose proof (IHc _ H H0).
-    destruct H2.
+    pose proof (IHc _ H H0) as H2.
+    destruct H2 as [x0 H2].
     exists (x0 + 1).
     rewrite <- (Nat.sub_add 4 x) in H1 at 1 by auto.
     replace (4 * c + 4 + x mod 4) with (4 * c + x mod 4 + 4) in H1 by omega.
@@ -265,7 +265,7 @@ Hint Rewrite eq_nat_dec_refl : natsimplify.
 (** Helper to get around the lack of function extensionality *)
 Definition eq_nat_dec_right_val n m (pf0 : n <> m) : { pf | eq_nat_dec n m = right pf }.
 Proof.
-  revert dependent n; induction m; destruct n as [|n]; simpl;
+  revert dependent n; induction m as [|m IHm]; destruct n as [|n]; simpl;
     intro pf0;
     [ (exists pf0; exfalso; abstract congruence)
     | eexists; reflexivity
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index 74fe96d6b..e99197ece 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -11,7 +11,7 @@ Lemma in_ZPGroup_range (n : Z) (n_pos : 1 < n) (p : Z) :
   List.In p (FGroup.s (ZPGroup n n_pos)) -> 1 <= p < n.
 Proof.
 unfold ZPGroup; simpl; intros Hin.
-pose proof (IGroup.isupport_incl Z (pmult n) (mkZp n) 1 Z.eq_dec).
+pose proof (IGroup.isupport_incl Z (pmult n) (mkZp n) 1 Z.eq_dec) as H.
 unfold List.incl in *.
 specialize (H p Hin).
 apply in_mkZp in H; auto.
@@ -29,7 +29,7 @@ Lemma generator_subgroup_is_group p (lt_1_p : 1 < p): forall y,
   -> forall a, List.In a (FGroup.s (ZPGroup p lt_1_p)) ->
   List.In a (EGroup.support Z.eq_dec y (ZPGroup p lt_1_p)).
 Proof.
-  intros.
+  intros y H a H0.
   destruct H as [in_ZPGroup_y y_order].
   pose proof (EGroup.support_incl_G Z Z.eq_dec (pmult p) y (ZPGroup p lt_1_p) in_ZPGroup_y).
   eapply Permutation.permutation_in; [|eauto].
@@ -67,7 +67,7 @@ Qed.
 
 Lemma p_odd : Z.odd p = true.
 Proof using neq_p_2 prime_p.
-  pose proof (Z.prime_odd_or_2 p prime_p).
+  pose proof (Z.prime_odd_or_2 p prime_p) as H.
   destruct H; auto.
 Qed.
 
@@ -82,7 +82,7 @@ Qed.
 Lemma fermat_little: forall a (a_nonzero : a mod p <> 0),
   a ^ (p - 1) mod p = 1.
 Proof using prime_p.
-  intros.
+  intros a a_nonzero.
   assert (rel_prime a p). {
     apply rel_prime_mod_rev; try prime_bound.
     assert (0 < p) as p_pos by prime_bound.
@@ -97,7 +97,7 @@ Qed.
 
 Lemma fermat_inv : forall a, a mod p <> 0 -> ((a^(p-2) mod p) * a) mod p = 1.
 Proof using prime_p.
-  intros.
+  intros a H.
   pose proof (prime_ge_2 _ prime_p).
   rewrite Zmult_mod_idemp_l.
   replace (a ^ (p - 2) * a) with (a^(p-1)).
@@ -120,7 +120,7 @@ Qed.
 Lemma euler_criterion_square_reverse : forall a (a_nonzero : a mod p <> 0),
   (exists b, b * b mod p = a) -> (a ^ x mod p = 1).
 Proof using Type*.
-  intros ? ? a_square.
+  intros a a_nonzero a_square.
   destruct a_square as [b a_square].
   assert (b mod p <> 0) as b_nonzero. {
     intuition.
@@ -170,7 +170,7 @@ Ltac ereplace x := match type of x with ?t =>
 Lemma euler_criterion_square : forall a (a_range : 1 <= a <= p - 1)
   (pow_a_x : a ^ x mod p = 1), exists b, b * b mod p = a.
 Proof using Type*.
-  intros.
+  intros a a_range pow_a_x.
   destruct (exists_primitive_root_power) as [y [in_ZPGroup_y [y_order gpow_y]]]; auto.
   destruct (gpow_y a a_range) as [j [j_range pow_y_j]]; clear gpow_y.
   rewrite Z.mod_pow in pow_a_x by prime_bound.
@@ -207,7 +207,7 @@ Qed.
 Lemma euler_criterion : forall a (a_range : 1 <= a <= p - 1),
   (a ^ x mod p = 1) <-> exists b, b * b mod p = a.
 Proof using Type*.
-  intros; split. {
+  intros a a_range; split. {
     exact (euler_criterion_square _ a_range).
   } {
     apply euler_criterion_square_reverse; auto.
@@ -219,21 +219,21 @@ Qed.
 Lemma euler_criterion_nonsquare : forall a (a_range : 1 <= a <= p - 1),
   (a ^ x mod p <> 1) <-> ~ (exists b, b * b mod p = a).
 Proof using Type*.
-  split; intros A B; apply (euler_criterion a a_range) in B; congruence.
+  intros a a_range; split; intros A B; apply (euler_criterion a a_range) in B; congruence.
 Qed.
 
 End EulerCriterion.
 
 Lemma divide2_1mod4 : forall x (x_1mod4 : x mod 4 = 1) (x_nonneg : 0 <= x), (2 | x / 2).
 Proof.
-  intros.
+  intros x x_1mod4 x_nonneg0.
   assert (Z.to_nat x mod 4 = 1)%nat as x_1mod4_nat. {
     replace 1 with (Z.of_nat 1) in * by auto.
     replace (x mod 4) with (Z.of_nat (Z.to_nat x mod 4)) in *
       by (rewrite mod_Zmod by omega; rewrite Z2Nat.id; auto).
     apply Nat2Z.inj in x_1mod4; auto.
   }
-  remember (Z.to_nat x / 4)%nat as c.
+  remember (Z.to_nat x / 4)%nat as c eqn:Heqc.
   destruct (divide2_1mod4_nat c (Z.to_nat x) Heqc x_1mod4_nat) as [k k_id].
   replace 2%nat with (Z.to_nat 2) in * by auto.
   apply inj_eq in k_id.
@@ -247,7 +247,7 @@ Qed.
 
 Lemma minus1_even_pow : forall x y, (2 | y) -> (1 < x) -> (0 <= y) -> ((x - 1) ^ y mod x = 1).
 Proof.
-  intros ? ? divide_2_y lt_1_x y_nonneg.
+  intros x y divide_2_y lt_1_x y_nonneg.
   apply Zdivide_Zdiv_eq in divide_2_y; try omega.
   rewrite divide_2_y.
   rewrite Z.pow_mul_r by omega.
@@ -261,7 +261,7 @@ Proof.
     do 2 rewrite Zmod_1_l by auto; auto.
   }
   rewrite <- (Z2Nat.id (y / 2)) by omega.
-  induction (Z.to_nat (y / 2)); try apply Zmod_1_l; auto.
+  induction (Z.to_nat (y / 2)) as [|n IHn]; try apply Zmod_1_l; auto.
   rewrite Nat2Z.inj_succ.
   rewrite Z.pow_succ_r by apply Zle_0_nat.
   rewrite Zmult_mod.
@@ -281,7 +281,7 @@ Qed.
 Lemma div2_p_1mod4 : forall (p : Z) (prime_p : prime p) (neq_p_2: p <> 2),
   (p / 2) * 2 + 1 = p.
 Proof.
-  intros.
+  intros p prime_p neq_p_2.
   destruct (Z.prime_odd_or_2 p prime_p); intuition.
   rewrite <- Zdiv2_div.
   pose proof (Zdiv2_odd_eqn p); break_match; break_match_hyps; congruence || omega.
@@ -290,7 +290,7 @@ Qed.
 Lemma minus1_square_1mod4 : forall (p : Z) (prime_p : prime p),
   (p mod 4 = 1)%Z -> exists b : Z, (b * b mod p = p - 1)%Z.
 Proof.
-  intros.
+  intros p prime_p H.
   assert (p <> 2) as neq_p_2 by (apply prime_1mod4_neq2; auto).
   apply (euler_criterion (p / 2) p prime_p).
   + auto.
diff --git a/src/Util/Relations.v b/src/Util/Relations.v
index d6b63b38f..8859a3bcc 100644
--- a/src/Util/Relations.v
+++ b/src/Util/Relations.v
@@ -38,7 +38,8 @@ Global Instance Equivalence_and {A B RA RB}
        {Equivalence_RB:@Equivalence B RB}
        : Equivalence (fun ab AB => RA (fst ab) (fst AB) /\ RB (snd ab) (snd AB)).
 Proof.
-  destruct Equivalence_RA as [], Equivalence_RB as []; cbv in *|-.
+  do 2 match goal with H : Equivalence _ |- _ => destruct H end;
+    cbv in *|-.
   repeat match goal with
            | _ => intro
            | _ => split
diff --git a/src/Util/Sum.v b/src/Util/Sum.v
index fe7fe662b..4d4fde6ac 100644
--- a/src/Util/Sum.v
+++ b/src/Util/Sum.v
@@ -10,10 +10,12 @@ Definition sumwise {A B} (RA:relation A) (RB : relation B) : relation (A + B)
                 | _, _ => False
                 end.
 
-Global Instance Equivalence_sumwise {A B} {RA:relation A} {RB:relation B}
-       {RA_equiv:Equivalence RA} {RB_equiv:Equivalence RB}
-  : Equivalence (sumwise RA RB).
+Global Instance Equivalence_sumwise
+  : forall {A B} {RA:relation A} {RB:relation B}
+           {RA_equiv:Equivalence RA} {RB_equiv:Equivalence RB},
+    Equivalence (sumwise RA RB).
 Proof.
+  intros A B RA RB RA_equiv RB_equiv.
   split; repeat intros [?|?]; simpl; trivial; destruct RA_equiv, RB_equiv; try tauto; eauto.
 Qed.
 
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 3fa0dabde..3f3c31fe2 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -137,7 +137,7 @@ end.
 
 Lemma to_list_from_list : forall {T} (n:nat) (xs:list T) pf, to_list n (from_list n xs pf) = xs.
 Proof.
-  destruct xs; simpl; intros; subst; auto.
+  destruct xs as [|t xs]; simpl; intros; subst; auto.
   generalize dependent t. simpl in *.
   induction xs; simpl in *; intros; congruence.
 Qed.
@@ -156,7 +156,7 @@ Lemma from_list'_to_list' : forall T n (xs:tuple' T n),
     forall x xs' pf, to_list' n xs = cons x xs' ->
       from_list' x n xs' pf = xs.
 Proof.
-  induction n; intros.
+  induction n; intros xs x xs' pf H.
   { simpl in *. injection H; clear H; intros; subst. congruence. }
   { destruct xs eqn:Hxs;
     destruct xs' eqn:Hxs';
@@ -166,7 +166,7 @@ Qed.
 
 Lemma from_list_to_list : forall {T n} (xs:tuple T n) pf, from_list n (to_list n xs) pf = xs.
 Proof.
-  destruct n; auto; intros; simpl in *.
+  destruct n as [|n]; auto; intros xs pf; simpl in *.
   { destruct xs; auto. }
   { destruct (to_list' n xs) eqn:H; try discriminate.
     eapply from_list'_to_list'; assumption. }
@@ -356,7 +356,9 @@ Lemma map_S' {n A B} (f:A -> B) (xs:tuple A (S n)) (x:A)
   : map (n:=S (S n)) f (xs, x) = (map (n:=S n) f xs, f x).
 Proof.
   tuple_maps_to_list_maps.
+  let lxs := match goal with lxs : list _ |- _ => lxs end in
   destruct lxs as [|x' lxs']; [simpl in *; discriminate|].
+  let x0 := match goal with H : _ = _ |- _ => H end in
   change ( f x :: List.map f (to_list (S n) (from_list (S n) (x' :: lxs') x0)) = f x :: to_list (S n) (map f (from_list (S n) (x' :: lxs') x0)) ).
   tuple_maps_to_list_maps.
   reflexivity.
@@ -369,7 +371,9 @@ Lemma map2_S' {n A B C} (f:A -> B -> C) (xs:tuple A (S n)) (ys:tuple B (S n)) (x
   : map2 (n:=S (S n)) f (xs, x) (ys, y) = (map2 (n:=S n) f xs ys, f x y).
 Proof.
   tuple_maps_to_list_maps.
+  let lxs := match goal with lxs : list A |- _ => lxs end in
   destruct lxs as [|x' lxs']; [simpl in *; discriminate|].
+  let lys := match goal with lxs : list B |- _ => lxs end in
   destruct lys as [|y' lys']; [simpl in *; discriminate|].
   change ( f x y ::  ListUtil.map2 f (to_list (S n) (from_list (S n) (x' :: lxs') x1))
     (to_list (S n) (from_list (S n) (y' :: lys') x0)) = f x y :: to_list (S n) (map2 f (from_list (S n) (x' :: lxs') x1) (from_list (S n) (y' :: lys') x0)) ).
@@ -497,13 +501,13 @@ Section Equivalence.
   Global Instance Equivalence_fieldwise' {R_equiv:Equivalence R} {n:nat} : Equivalence (fieldwise' n R).
   Proof using Type. constructor; exact _. Qed.
 
-  Global Instance Reflexive_fieldwise {R_Reflexive:Reflexive R} {n:nat} : Reflexive (fieldwise n R) | 5.
+  Global Instance Reflexive_fieldwise {R_Reflexive:Reflexive R} : forall {n:nat}, Reflexive (fieldwise n R) | 5.
   Proof using Type. destruct n; (repeat constructor || exact _). Qed.
-  Global Instance Symmetric_fieldwise {R_Symmetric:Symmetric R} {n:nat} : Symmetric (fieldwise n R) | 5.
+  Global Instance Symmetric_fieldwise {R_Symmetric:Symmetric R} : forall {n:nat}, Symmetric (fieldwise n R) | 5.
   Proof using Type. destruct n; (repeat constructor || exact _). Qed.
-  Global Instance Transitive_fieldwise {R_Transitive:Transitive R} {n:nat} : Transitive (fieldwise n R) | 5.
+  Global Instance Transitive_fieldwise {R_Transitive:Transitive R} : forall {n:nat}, Transitive (fieldwise n R) | 5.
   Proof using Type. destruct n; (repeat constructor || exact _). Qed.
-  Global Instance Equivalence_fieldwise {R_equiv:Equivalence R} {n:nat} : Equivalence (fieldwise n R).
+  Global Instance Equivalence_fieldwise {R_equiv:Equivalence R} : forall {n:nat}, Equivalence (fieldwise n R).
   Proof using Type. constructor; exact _. Qed.
 End Equivalence.
 
@@ -511,7 +515,7 @@ Arguments fieldwise' {A B n} _ _ _.
 Arguments fieldwise {A B n} _ _ _.
 
 Local Hint Extern 0 => solve [ solve_decidable_transparent ] : typeclass_instances.
-Global Instance dec_fieldwise' {A RA} {HA : DecidableRel RA} {n} : DecidableRel (@fieldwise' A A n RA) | 10.
+Global Instance dec_fieldwise' {A RA} {HA : DecidableRel RA} : forall {n}, DecidableRel (@fieldwise' A A n RA) | 10.
 Proof.
   induction n; simpl @fieldwise'.
   { exact _. }
@@ -519,7 +523,7 @@ Proof.
     exact _. }
 Defined.
 
-Global Instance dec_fieldwise {A RA} {HA : DecidableRel RA} {n} : DecidableRel (@fieldwise A A n RA) | 10.
+Global Instance dec_fieldwise {A RA} {HA : DecidableRel RA} : forall {n}, DecidableRel (@fieldwise A A n RA) | 10.
 Proof.
   destruct n; unfold fieldwise; exact _.
 Defined.
@@ -574,7 +578,7 @@ Lemma fieldwiseb'_fieldwise' :forall {A B} n R Rb
   (forall a b, Rb a b = true <-> R a b) ->
   (fieldwiseb' Rb a b = true <-> fieldwise' R a b).
 Proof.
-  intros.
+  intros A B n R Rb a b H.
   revert n a b;
   induction n; intros; simpl @tuple' in *;
     simpl fieldwiseb'; simpl fieldwise'; auto.
@@ -588,7 +592,7 @@ Lemma fieldwiseb_fieldwise :forall {A B} n R Rb
   (forall a b, Rb a b = true <-> R a b) ->
   (fieldwiseb Rb a b = true <-> fieldwise R a b).
 Proof.
-  intros; destruct n; simpl @tuple in *;
+  intros A B n R Rb a b H; destruct n; simpl @tuple in *;
     simpl @fieldwiseb; simpl @fieldwise; try tauto.
   auto using fieldwiseb'_fieldwise'.
 Qed.
@@ -617,7 +621,7 @@ end.
 Lemma from_list_default'_eq : forall {T} (d : T) xs n y pf,
   from_list_default' d y n xs = from_list' y n xs pf.
 Proof.
-  induction xs; destruct n; intros; simpl in *;
+  induction xs as [|?? IHxs]; destruct n; intros; simpl in *;
     solve [ congruence (* 8.5 *)
           | erewrite IHxs; reflexivity ]. (* 8.4 *)
 Qed.
@@ -652,7 +656,7 @@ Require Import Coq.Lists.SetoidList.
 Lemma fieldwise_to_list_iff : forall {T n} R (s t : tuple T n),
     (fieldwise R s t <-> Forall2 R (to_list _ s) (to_list _ t)).
 Proof.
-  induction n; split; intros.
+  induction n as [|n IHn]; intros R s t; split; intros.
   + constructor.
   + cbv [fieldwise]. auto.
   + destruct n; cbv [tuple to_list fieldwise] in *.
@@ -774,7 +778,7 @@ Lemma from_list_cons {A n}:
   forall (xs : list A) a (H:length (a::xs)=S n),
   from_list (S n) (a :: xs) H = append a (from_list n xs (length_cons_full _ _ _ H)).
 Proof.
-  destruct n; intros; destruct xs; distr_length; [reflexivity|].
+  destruct n; intros xs a H; destruct xs; distr_length; [reflexivity|].
   cbv [from_list]; rewrite !from_list'_cons.
   rewrite <-!from_list_default'_eq with (d:=a).
   reflexivity.
@@ -904,7 +908,7 @@ Lemma mapi_with'_left_step {T A B n} f a0:
                            (fst (mapi_with' i f start xs)) a0))
                    (snd (mapi_with' i f start xs))).
 Proof.
-  induction n; intros; [subst; simpl; repeat f_equal; omega|].
+  induction n as [|? IHn]; intros; [subst; simpl; repeat f_equal; omega|].
   rewrite mapi_with'_step; autorewrite with cancel_pair.
   rewrite tl_left_append, hd_left_append.
   erewrite IHn by reflexivity; subst; autorewrite with cancel_pair.
@@ -951,12 +955,12 @@ Proof.
 Qed.
 
 Lemma to_list_repeat {A} (a:A) n : to_list _ (repeat a n) = List.repeat a n.
-Proof. induction n; [reflexivity|destruct n; simpl in *; congruence]. Qed.
+Proof. induction n as [|n]; [reflexivity|destruct n; simpl in *; congruence]. Qed.
 
 
-Global Instance map'_Proper {n A B} : Proper (pointwise_relation _ eq ==> eq ==> eq) (fun f => @map' A B f n) | 10.
+Global Instance map'_Proper : forall {n A B}, Proper (pointwise_relation _ eq ==> eq ==> eq) (fun f => @map' A B f n) | 10.
 Proof.
-  induction n.
+  induction n as [|n IHn]; intros.
   { compute; intros; subst; auto. }
   { cbv [pointwise_relation Proper respectful] in *.
     intros f g Hfg x y ?; subst y.
@@ -964,8 +968,8 @@ Proof.
     congruence. }
 Qed.
 
-Global Instance map_Proper {n A B} : Proper (pointwise_relation _ eq ==> eq ==> eq) (@map n A B) | 10.
+Global Instance map_Proper : forall {n A B}, Proper (pointwise_relation _ eq ==> eq ==> eq) (@map n A B) | 10.
 Proof.
-  destruct n; [ | apply map'_Proper ].
+  destruct n; intros; [ | apply map'_Proper ].
   { repeat (intros [] || intro); auto. }
 Qed.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index c8aa9a4e5..64cfda434 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -66,9 +66,9 @@ Module Word.
   Theorem weqb_hetero_homo_true_iff : forall sz x y,
       @weqb_hetero sz sz x y = true <-> x = y.
   Proof.
-    etransitivity; [ apply weqb_hetero_true_iff | ].
+    intros sz x y; etransitivity; [ apply weqb_hetero_true_iff | ].
     split; [ intros [pf H] | intro ]; try (subst y; exists eq_refl; reflexivity).
-    revert y H; induction x as [|b n x IHx]; intros.
+    revert y H; induction x as [|b n x IHx]; intros y H.
     { subst y;
         refine match pf in (_ = z)
                      return match z return 0 = z -> Prop with
@@ -184,7 +184,7 @@ Section Pow2.
 
   Lemma Zpow_pow2 : forall n, pow2 n = Z.to_nat (2 ^ (Z.of_nat n)).
   Proof.
-    induction n; intros; auto.
+    induction n as [|n IHn]; intros; auto.
     simpl pow2.
     rewrite Nat2Z.inj_succ.
     rewrite Z.pow_succ_r by apply Zle_0_nat.
@@ -196,7 +196,7 @@ Section Pow2.
 
   Lemma Npow2_gt0 : forall x, (0 < Npow2 x)%N.
   Proof.
-    intros; induction x.
+    intros x; induction x as [|x IHx].
 
     - simpl; apply N.lt_1_r; intuition.
 
@@ -218,7 +218,7 @@ Section Pow2.
 
   Lemma Npow2_N: forall n, Npow2 n = (2 ^ N.of_nat n)%N.
   Proof.
-    induction n.
+    induction n as [|n IHn].
 
     - simpl; intuition.
 
@@ -232,7 +232,7 @@ Section Pow2.
       (Z.log2 (Z.of_N x) < Z.of_nat n)%Z
    -> (x < Npow2 n)%N.
   Proof.
-    intros.
+    intros x n H.
     apply N2Z.inj_lt.
     rewrite Npow2_N, N2Z.inj_pow, nat_N_Z.
     destruct (N.eq_dec x 0%N) as [e|e].
@@ -247,7 +247,7 @@ Section Pow2.
 
   Lemma Npow2_ordered: forall n m, (n <= m)%nat -> (Npow2 n <= Npow2 m)%N.
   Proof.
-    induction n; intros m H; try rewrite Npow2_succ.
+    induction n as [|n IHn]; intros m H; try rewrite Npow2_succ.
 
     - simpl; apply Npow2_ge1.
 
@@ -299,7 +299,7 @@ Section WordToN.
   Lemma wbit_large {n} (x: word n) (k: nat)
     : n <= k -> wbit x k = false.
   Proof.
-    revert k; induction x, k; intro H; simpl; try reflexivity; try omega.
+    revert k; induction x as [|b n x IHx], k; intro H; simpl; try reflexivity; try omega.
     apply IHx; omega.
   Qed.
 
@@ -354,17 +354,17 @@ Section WordToN.
             end = N.double x) as kill_match by (
       induction x; simpl; intuition).
 
-    induction n; intros.
+    induction n as [|n IHn]; intros x k.
 
     - shatter x; simpl; intuition.
 
     - revert IHn; rewrite <- (N2Nat.id k).
-      generalize (N.to_nat k) as k'; intros; clear k.
+      generalize (N.to_nat k) as k'; intros k' IHn; clear k.
       rewrite Nat2N.id in *.
 
-      induction k'.
+      induction k' as [|k' IHk'].
 
-      + clear IHn; induction x; simpl; intuition.
+      + clear IHn; induction x as [|b ? x IHx]; simpl; intuition.
         destruct (wordToN x), b; simpl; intuition.
 
       + clear IHk'.
@@ -386,10 +386,11 @@ Section WordToN.
         destruct (whd x);
           try rewrite N.testbit_odd_succ;
           try rewrite N.testbit_even_succ;
+          let k' := k' in
           try abstract (
             unfold N.le; simpl;
             induction (N.of_nat k'); intuition;
-            try inversion H);
+            match goal with H : _ |- _ => solve [ inversion H ] end);
           rewrite IHn;
           rewrite Nat2N.id;
           reflexivity.
@@ -400,7 +401,7 @@ Section WordToN.
                               then N.testbit v (N.of_nat k)
                               else false.
   Proof.
-    revert k v; induction sz, k; intros; try reflexivity.
+    revert k v; induction sz as [|sz IHsz], k; intros v **; try reflexivity.
     { destruct v as [|p]; simpl; try reflexivity.
       destruct p; simpl; reflexivity. }
     { pose proof (fun v k => IHsz k (Npos v)) as IHszp.
@@ -483,7 +484,7 @@ Section WordToN.
   Lemma wordToN_split1: forall {n m} x,
     wordToN (@split1 n m x) = N.land (wordToN x) (wordToN (wones n)).
   Proof.
-    intros.
+    intros n m x.
 
     pose proof (Word.combine_split _ _ x) as C; revert C.
     generalize (split1 n m x) as a, (split2 n m x) as b.
@@ -494,7 +495,7 @@ Section WordToN.
     repeat rewrite wordToN_testbit.
     revert x a b.
 
-    induction n, m; intros;
+    induction n as [|n IHn], m; intros;
       shatter a; shatter b;
       induction (N.to_nat x) as [|n0];
       try rewrite <- (Nat2N.id n0);
@@ -506,7 +507,7 @@ Section WordToN.
   Lemma wordToN_split2: forall {n m} x,
     wordToN (@split2 n m x) = N.shiftr (wordToN x) (N.of_nat n).
   Proof.
-    intros.
+    intros n m x.
 
     pose proof (Word.combine_split _ _ x) as C; revert C.
     generalize (split1 n m x) as a, (split2 n m x) as b.
@@ -519,7 +520,7 @@ Section WordToN.
       try apply N_ge_0.
 
     revert x a b.
-    induction n, m; intros;
+    induction n as [|n IHn], m; intros;
       shatter a;
       try apply N_ge_0.
 
@@ -545,7 +546,7 @@ Section WordToN.
 
   Lemma wordToN_wones: forall x, wordToN (wones x) = N.ones (N.of_nat x).
   Proof.
-    induction x.
+    induction x as [|x IHx].
 
     - simpl; intuition.
 
@@ -576,7 +577,7 @@ Section WordToN.
     wordToN (@Word.combine n a m b)
       = N.lxor (N.shiftl (wordToN b) (N.of_nat n)) (wordToN a).
   Proof.
-    intros; symmetry.
+    intros n m a b; symmetry.
 
     replaceAt1 a with (Word.split1 _ _ (Word.combine a b))
       by (apply Word.split1_combine).
@@ -608,7 +609,7 @@ Section WordToN.
   Lemma NToWord_equal: forall n (x y: word n),
       wordToN x = wordToN y -> x = y.
   Proof.
-    intros.
+    intros n x y H.
     rewrite <- (NToWord_wordToN _ x).
     rewrite <- (NToWord_wordToN _ y).
     rewrite H; reflexivity.
@@ -617,7 +618,7 @@ Section WordToN.
   Lemma Npow2_ignore: forall {n} (x: word n),
     x = NToWord _ (wordToN x + Npow2 n).
   Proof.
-    intros.
+    intros n x.
     rewrite <- (NToWord_wordToN n x) at 1.
     repeat rewrite NToWord_nat.
     rewrite N2Nat.inj_add.
@@ -632,7 +633,7 @@ End WordToN.
 Section WordBounds.
   Lemma word_size_bound : forall {n} (w: word n), (wordToN w < Npow2 n)%N.
   Proof.
-    intros; pose proof (wordToNat_bound w) as B;
+    intros n w; pose proof (wordToNat_bound w) as B;
       rewrite of_nat_lt in B;
       rewrite <- Npow2_nat in B;
       rewrite N2Nat.id in B;
@@ -714,13 +715,13 @@ Section WordBounds.
   Lemma wordize_and: forall {n} (x y: word n),
     wordToN (wand x y) = N.land (wordToN x) (wordToN y).
   Proof.
-    intros.
+    intros n x y.
     apply N.bits_inj_iff; unfold N.eqf; intro k.
     rewrite N.land_spec.
     repeat rewrite wordToN_testbit.
     revert x y.
     generalize (N.to_nat k) as k'.
-    induction n; intros; shatter x; shatter y; simpl; [reflexivity|].
+    induction n as [|n IHn]; intros; shatter x; shatter y; simpl; [reflexivity|].
     induction k'; [reflexivity|].
     fold wand.
     rewrite IHn.
@@ -730,13 +731,13 @@ Section WordBounds.
   Lemma wordize_or: forall {n} (x y: word n),
     wordToN (wor x y) = N.lor (wordToN x) (wordToN y).
   Proof.
-    intros.
+    intros n x y.
     apply N.bits_inj_iff; unfold N.eqf; intro k.
     rewrite N.lor_spec.
     repeat rewrite wordToN_testbit.
     revert x y.
     generalize (N.to_nat k) as k'; clear k.
-    induction n; intros; shatter x; shatter y; simpl; [reflexivity|].
+    induction n as [|n IHn]; intros; shatter x; shatter y; simpl; [reflexivity|].
     induction k'; [reflexivity|].
     rewrite IHn.
     reflexivity.
@@ -756,7 +757,7 @@ Qed.
 
 Lemma weqb_false_iff : forall sz (x y : word sz), weqb x y = false <-> x <> y.
 Proof.
-  split; intros.
+  intros sz x y; split; intros.
   + intro eq_xy; apply weqb_true_iff in eq_xy; congruence.
   + case_eq (weqb x y); intros weqb_xy; auto.
     apply weqb_true_iff in weqb_xy.
@@ -786,7 +787,7 @@ Fixpoint correct_wordsize_eq (x y : nat) : wordsize_eq x y -> x = y
 
 Lemma correct_wordsize_eq_refl n pf : correct_wordsize_eq n n pf = eq_refl.
 Proof.
-  induction n; [ reflexivity | simpl ].
+  induction n as [|n IHn]; [ reflexivity | simpl ].
   rewrite IHn; reflexivity.
 Qed.
 
@@ -827,13 +828,13 @@ Definition clearbit {b} n {H:n < b} (w:word b) : word b :=
 
 Lemma wordToNat_wzero {n} : wordToNat (wzero n) = 0.
 Proof.
-  unfold wzero; induction n; simpl; try rewrite_hyp!*; omega.
+  unfold wzero; induction n as [|n IHn]; simpl; try rewrite_hyp!*; omega.
 Qed.
 
 Lemma wordToNat_combine : forall {a} (wa:word a) {b} (wb:word b),
   wordToNat (wa ++ wb) = wordToNat wa + 2^a * wordToNat wb.
 Proof.
-  induction wa; intros; simpl; rewrite ?IHwa; break_match; nia.
+  induction wa as [|??? IHwa]; intros; simpl; rewrite ?IHwa; break_match; nia.
 Qed.
 
 Lemma wordToNat_zext_ge {n m pf} (w:word m) : wordToNat (@zext_ge n m pf w) = wordToNat w.
@@ -853,7 +854,7 @@ Proof.
            | _ => I
            end.
     reflexivity. }
-  { intros; rewrite IHx; clear IHx; revert x.
+  { intros x' y y'; rewrite IHx; clear IHx; revert x.
     refine match x' in word Sn return match Sn return word Sn -> _ with
                                       | 0 => fun _ => True
                                       | S _ => fun x' => forall x, WS (f b' (whd x')) (bitwp f (x ++ y) (wtl x' ++ y')) = WS (f b' (whd (x' ++ y'))) (bitwp f (x ++ y) (wtl (x' ++ y')))
@@ -897,7 +898,7 @@ Proof.
       rewrite pow2_id in *.
   { assert (b - c = 0) by omega.
     assert (2^b <= 2^c) by auto using pow_le_mono_r with arith.
-    generalize dependent (b - c); intros; destruct x0; try omega; [].
+    generalize dependent (b - c); intros n x0 H0 H2; destruct x0; try omega; [].
     simpl; rewrite mul_0_r, add_0_r.
     rewrite mod_small by omega.
     omega. }
@@ -929,7 +930,7 @@ Proof.
       rewrite pow2_id in *.
   { assert (b - c = 0) by omega.
     assert (2^b <= 2^c) by auto using pow_le_mono_r with arith.
-    generalize dependent (b - c); intros; destruct x0; try omega.
+    generalize dependent (b - c); intros n x0 H0 H2; destruct x0; try omega.
     simpl; rewrite mul_0_r, add_0_r.
     rewrite mod_small by omega.
     omega. }
@@ -939,9 +940,9 @@ Qed.
 
 Lemma wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w) mod (2^a).
 Proof.
-  intro a; induction a.
+  intro a; induction a as [|a IHa].
   { reflexivity. }
-  { simpl; intros; rewrite IHa; clear IHa.
+  { simpl; intros b w; rewrite IHa; clear IHa.
     rewrite (shatter_word w); simpl.
     change (2^a + (2^a + 0)) with (2 * 2^a).
     rewrite (mul_comm 2 (2^a)).
@@ -983,7 +984,7 @@ Section Bounds.
 
   Lemma wordToN_wplus : bounds_2statement (@wplus _) Z.add.
   Proof.
-    intros.
+    intros sz x y H H0.
     rewrite <- wordize_plus; [rewrite N2Z.inj_add; reflexivity|].
     destruct (N.eq_dec (wordToN x + wordToN y) 0%N) as [e|e];
         [rewrite e; apply Npow2_gt0|].
@@ -1014,7 +1015,7 @@ Section Bounds.
 
   Lemma wordToN_wmult : bounds_2statement (@wmult _) Z.mul.
   Proof.
-    intros.
+    intros sz x y H H0.
     rewrite <- wordize_mult; [rewrite N2Z.inj_mul; reflexivity|].
     destruct (N.eq_dec (wordToN x * wordToN y) 0%N) as [e|e];
         [rewrite e; apply Npow2_gt0|].
@@ -1277,7 +1278,7 @@ Arguments wlast {_} _.
 Lemma combine_winit_wlast : forall {sz} a b (c:word (sz+1)),
     @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO).
 Proof.
-  intros; split; unfold winit, wlast; intro H.
+  intros sz a b c; split; unfold winit, wlast; intro H.
 
   - rewrite <- H.
     rewrite split1_combine, split2_combine.
@@ -1289,7 +1290,7 @@ Proof.
   - destruct H as [H0 H1]; rewrite H0.
     replace b with (split2 sz 1 c); [apply combine_split|].
     rewrite H1.
-    generalize (split2 sz 1 c) as b'; intro.
+    generalize (split2 sz 1 c) as b'; intro b'.
     shatter b'.
     generalize (wtl b') as b''; intro;
       shatter b''; reflexivity.
@@ -1309,7 +1310,7 @@ Qed.
 Lemma WordNZ_split1 : forall {n m} w,
     Z.of_N (Word.wordToN (Word.split1 n m w)) = Z.pow2_mod (Z.of_N (Word.wordToN w)) (Z.of_nat n).
 Proof.
-  intros; unfold Z.pow2_mod.
+  intros n m w; unfold Z.pow2_mod.
   rewrite wordToN_split1.
   apply Z.bits_inj_iff'; intros k Hpos.
   rewrite Z.land_spec.
@@ -1324,28 +1325,28 @@ Proof.
     apply Z2N.inj_le; [apply Nat2Z.is_nonneg|assumption|].
     etransitivity; [|apply N.ge_le; eassumption].
     apply N.eq_le_incl.
-    induction n; simpl; reflexivity.
+    induction n as [|n IHn]; simpl; reflexivity.
 
   - rewrite Z.ones_spec_low, N.ones_spec_low;
       [reflexivity|assumption|split; [omega|]].
     apply Z2N.inj_lt; [assumption|apply Nat2Z.is_nonneg|].
     eapply N.lt_le_trans; [eassumption|].
     apply N.eq_le_incl.
-    induction n; simpl; reflexivity.
+    induction n as [|n IHn]; simpl; reflexivity.
 Qed.
 
 (* TODO : automate *)
 Lemma WordNZ_split2 : forall {n m} w,
     Z.of_N (Word.wordToN (Word.split2 n m w)) = Z.shiftr (Z.of_N (Word.wordToN w)) (Z.of_nat n).
 Proof.
-  intros; unfold Z.pow2_mod.
+  intros n m w; unfold Z.pow2_mod.
   rewrite wordToN_split2.
   apply Z.bits_inj_iff'; intros k Hpos.
   rewrite Z2N.inj_testbit; [|assumption].
   rewrite Z.shiftr_spec, N.shiftr_spec; [|apply N2Z.inj_le; rewrite Z2N.id|]; try assumption.
   rewrite Z2N.inj_testbit; [f_equal|omega].
   rewrite Z2N.inj_add; [f_equal|assumption|apply Nat2Z.is_nonneg].
-  induction n; simpl; reflexivity.
+  induction n as [|n IHn]; simpl; reflexivity.
 Qed.
 
 Lemma WordNZ_range : forall {n} B w,
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 936b4ce76..01e125e00 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -53,7 +53,7 @@ Module Z.
   Lemma pos_pow_nat_pos : forall x n,
     Z.pos x ^ Z.of_nat n > 0.
   Proof.
-    do 2 (intros; induction n; subst; simpl in *; auto with zarith).
+    do 2 (try intros x n; induction n as [|n]; subst; simpl in *; auto with zarith).
     rewrite <- Pos.add_1_r, Zpower_pos_is_exp.
     apply Zmult_gt_0_compat; auto; reflexivity.
   Qed.
@@ -64,7 +64,7 @@ Module Z.
   Lemma pow_Z2N_Zpow : forall a n, 0 <= a ->
     ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat.
   Proof.
-    intros; induction n; try reflexivity.
+    intros a n H; induction n as [|n IHn]; try reflexivity.
     rewrite Nat2Z.inj_succ.
     rewrite pow_succ_r by apply le_0_n.
     rewrite Z.pow_succ_r by apply Zle_0_nat.
@@ -94,14 +94,14 @@ Module Z.
 
   Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true.
   Proof.
-    intro; split. {
+    intros n; split. {
       intro divide2_n.
       Z.divide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega].
       rewrite divide2_n.
       apply Z.even_mul.
     } {
       intro n_even.
-      pose proof (Zmod_even n).
+      pose proof (Zmod_even n) as H.
       rewrite n_even in H.
       apply Zmod_divide; omega || auto.
     }
@@ -109,7 +109,7 @@ Module Z.
 
   Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true.
   Proof.
-    intros.
+    intros p prime_p.
     apply Decidable.imp_not_l; try apply Z.eq_decidable.
     intros p_neq2.
     pose proof (Zmod_odd p) as mod_odd.
@@ -127,7 +127,7 @@ Module Z.
   Lemma shiftr_add_shiftl_high : forall n m a b, 0 <= n <= m -> 0 <= a < 2 ^ n ->
     Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr b (m - n).
   Proof.
-    intros.
+    intros n m a b H H0.
     rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2 by omega.
     replace (2 ^ m) with (2 ^ n * 2 ^ (m - n)) by
       (rewrite <-Z.pow_add_r by omega; f_equal; ring).
@@ -141,7 +141,7 @@ Module Z.
   Lemma shiftr_add_shiftl_low : forall n m a b, 0 <= m <= n -> 0 <= a < 2 ^ n ->
     Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr a m + Z.shiftr b (m - n).
   Proof.
-    intros.
+    intros n m a b H H0.
     rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2, Z.shiftr_mul_pow2 by omega.
     replace (2 ^ n) with (2 ^ (n - m) * 2 ^ m) by
       (rewrite <-Z.pow_add_r by omega; f_equal; ring).
@@ -155,8 +155,8 @@ Module Z.
     0 <= a < 2 ^ n ->
     Z.testbit (a + Z.shiftl b n) i = Z.testbit b (i - n).
   Proof.
-    intros ? ?.
-    apply natlike_ind with (x := i); intros; try assumption;
+    intros i ?.
+    apply natlike_ind with (x := i); [ intros a b n | intros x H0 H1 a b n | ]; intros; try assumption;
       (destruct (Z_eq_dec 0 n); [ subst; rewrite Z.pow_0_r in *;
        replace a with 0 by omega; f_equal; ring | ]); try omega.
     rewrite <-Z.add_1_r at 1. rewrite <-Z.shiftr_spec by assumption.
@@ -195,7 +195,7 @@ Module Z.
   Lemma land_add_land : forall n m a b, (m <= n)%nat ->
     Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)).
   Proof.
-    intros.
+    intros n m a b H.
     rewrite !Z.land_ones by apply Nat2Z.is_nonneg.
     rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg.
     replace (b * 2 ^ Z.of_nat n) with
@@ -232,7 +232,7 @@ Module Z.
   Lemma pow2_lt_or_divides : forall a b, 0 <= b ->
     2 ^ a < 2 ^ b \/ (2 ^ a) mod 2 ^ b = 0.
   Proof.
-    intros.
+    intros a b H.
     destruct (Z_lt_dec a b); [left|right].
     { apply Z.pow_lt_mono_r; auto; omega. }
     { replace a with (a - b + b) by ring.
@@ -243,7 +243,7 @@ Module Z.
   Lemma odd_mod : forall a b, (b <> 0)%Z ->
     Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a.
   Proof.
-    intros.
+    intros a b H.
     rewrite Zmod_eq_full by assumption.
     rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul.
     case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r.
@@ -251,7 +251,7 @@ Module Z.
 
   Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0.
   Proof.
-    intros.
+    intros a b c H.
     replace b with (b - c + c) by ring.
     rewrite Z.pow_add_r by omega.
     apply Z_mod_mult.
@@ -287,14 +287,14 @@ Module Z.
 
   Lemma shiftr_le : forall a b i : Z, 0 <= i -> a <= b -> a >> i <= b >> i.
   Proof.
-    intros until 1. revert a b. apply natlike_ind with (x := i); intros; auto.
+    intros a b i ?; revert a b. apply natlike_ind with (x := i); intros; auto.
     rewrite !shiftr_succ, shiftr_1_r_le; eauto. reflexivity.
   Qed.
   Hint Resolve shiftr_le : zarith.
 
   Lemma ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1.
   Proof.
-    induction i; [ | | pose proof (Pos2Z.neg_is_neg p) ]; try omega.
+    induction i as [|p|p]; [ | | pose proof (Pos2Z.neg_is_neg p) ]; try omega.
     intros.
     unfold Z.ones.
     rewrite !Z.shiftl_1_l, Z.shiftr_div_pow2, <-!Z.sub_1_r, Z.pow_1_r, <-!Z.add_opp_r by omega.
@@ -310,12 +310,12 @@ Module Z.
   Lemma shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) ->
     Z.shiftr a i <= Z.ones (n - i) \/ n <= i.
   Proof.
-    intros until 1.
+    intros a n H.
     apply natlike_ind.
     + unfold Z.ones.
       rewrite Z.shiftr_0_r, Z.shiftl_1_l, Z.sub_0_r.
       omega.
-    + intros.
+    + intros x H0 H1.
       destruct (Z_lt_le_dec x n); try omega.
       intuition auto with zarith lia.
       left.
@@ -360,7 +360,7 @@ Module Z.
   Lemma lor_shiftl : forall a b n, 0 <= n -> 0 <= a < 2 ^ n ->
     Z.lor a (Z.shiftl b n) = a + (Z.shiftl b n).
   Proof.
-    intros.
+    intros a b n H H0.
     apply Z.bits_inj'; intros t ?.
     rewrite Z.lor_spec, Z.shiftl_spec by assumption.
     destruct (Z_lt_dec t n).
@@ -449,7 +449,7 @@ Module Z.
   Lemma pow2_mod_id_iff : forall a n, 0 <= n ->
                                       (Z.pow2_mod a n = a <-> 0 <= a < 2 ^ n).
   Proof.
-    intros.
+    intros a n H.
     rewrite Z.pow2_mod_spec by assumption.
     assert (0 < 2 ^ n) by Z.zero_bounds.
     rewrite Z.mod_small_iff by omega.
@@ -460,8 +460,8 @@ Module Z.
     (forall n, ~ (n < x) -> Z.testbit a n = false) ->
     a < 2 ^ x.
   Proof.
-    intros.
-    assert (a = Z.pow2_mod a x). {
+    intros a x H H0.
+    assert (H1 : a = Z.pow2_mod a x). {
      apply Z.bits_inj'; intros.
      rewrite Z.testbit_pow2_mod by omega; break_match; auto.
     }
@@ -472,7 +472,7 @@ Module Z.
   Lemma lor_range : forall x y n, 0 <= x < 2 ^ n -> 0 <= y < 2 ^ n ->
                                   0 <= Z.lor x y < 2 ^ n.
   Proof.
-    intros; assert (0 <= n) by auto with zarith omega.
+    intros x y n H H0; assert (0 <= n) by auto with zarith omega.
     repeat match goal with
            | |- _ => progress intros
            | |- _ => rewrite Z.lor_spec
@@ -493,7 +493,7 @@ Module Z.
       (0 <= y < 2 ^ n)%Z ->
       (0 <= Z.lor y (Z.shiftl x n) < 2 ^ (n + m))%Z.
   Proof.
-    intros.
+    intros x y n m H H0 H1 H2.
     apply Z.lor_range.
     { split; try omega.
       apply Z.lt_le_trans with (m := (2 ^ n)%Z); try omega.
@@ -512,8 +512,8 @@ Module Z.
 
   Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N.
   Proof.
-    induction a; destruct b; intros; try solve [cbv; congruence];
-      simpl; specialize (IHa b); case_eq (Pos.land a b); intro; simpl;
+    induction a as [a IHa|a IHa|]; destruct b as [b|b|]; try solve [cbv; congruence];
+      simpl; specialize (IHa b); case_eq (Pos.land a b); intro p; simpl;
       try (apply N_le_1_l || apply N.le_0_l); intro land_eq;
       rewrite land_eq in *; unfold N.le, N.compare in *;
       rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO;
@@ -524,7 +524,7 @@ Module Z.
   Lemma land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) ->
     Z.land a b <= a.
   Proof.
-    intros.
+    intros a b H H0.
     destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence].
     cbv [Z.land].
     rewrite <-N2Z.inj_pos, <-N2Z.inj_le.
@@ -542,7 +542,7 @@ Module Z.
   Lemma le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) ->
     In x l -> x <= fold_right Z.max low l.
   Proof.
-    induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ].
+    induction l as [|a l IHl]; intros ? lower_bound In_list; [cbv [In] in *; intuition | ].
     simpl.
     destruct (in_inv In_list); subst.
     + apply Z.le_max_l.
@@ -553,13 +553,13 @@ Module Z.
 
   Lemma le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l.
   Proof.
-    induction l; intros; try reflexivity.
+    induction l as [|a l IHl]; intros; try reflexivity.
     etransitivity; [ apply IHl | apply Z.le_max_r ].
   Qed.
 
   Lemma add_compare_mono_r: forall n m p, (n + p ?= m + p) = (n ?= m).
   Proof.
-    intros.
+    intros n m p.
     rewrite <-!(Z.add_comm p).
     apply Z.add_compare_mono_l.
   Qed.
@@ -997,7 +997,7 @@ Module Z.
 
   Lemma lt_mul_2_mod_sub : forall a b, b <> 0 -> b <= a < 2 * b -> a mod b = a - b.
   Proof.
-    intros.
+    intros a b H H0.
     replace (a mod b) with ((1 * b + (a - b)) mod b) by (f_equal; ring).
     rewrite Z.mod_add_l by auto.
     apply Z.mod_small.
@@ -1093,7 +1093,7 @@ Module Z.
 
   Lemma lt_pow_2_shiftr : forall a n, 0 <= a < 2 ^ n -> a >> n = 0.
   Proof.
-    intros.
+    intros a n H.
     destruct (Z_le_dec 0 n).
     + rewrite Z.shiftr_div_pow2 by assumption.
       auto using Z.div_small.
@@ -1118,7 +1118,7 @@ Module Z.
   Lemma lt_mul_2_pow_2_shiftr : forall a n, 0 <= a < 2 * 2 ^ n ->
                                             a >> n = if Z_lt_dec a (2 ^ n) then 0 else 1.
   Proof.
-    intros; break_match; [ apply lt_pow_2_shiftr; omega | ].
+    intros a n H; break_match; [ apply lt_pow_2_shiftr; omega | ].
     destruct (Z_le_dec 0 n).
     + replace (2 * 2 ^ n) with (2 ^ (n + 1)) in *
         by (rewrite Z.pow_add_r; try omega; ring).
@@ -1217,7 +1217,7 @@ Module Z.
   Section ZInequalities.
     Lemma land_le : forall x y, (0 <= x)%Z -> (Z.land x y <= x)%Z.
     Proof.
-      intros; apply Z.ldiff_le; [assumption|].
+      intros x y H; apply Z.ldiff_le; [assumption|].
       rewrite Z.ldiff_land, Z.land_comm, Z.land_assoc.
       rewrite <- Z.land_0_l with (a := y); f_equal.
       rewrite Z.land_comm, Z.land_lnot_diag.
@@ -1226,7 +1226,7 @@ Module Z.
 
     Lemma lor_lower : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> (x <= Z.lor x y)%Z.
     Proof.
-      intros; apply Z.ldiff_le; [apply Z.lor_nonneg; auto|].
+      intros x y H H0; apply Z.ldiff_le; [apply Z.lor_nonneg; auto|].
       rewrite Z.ldiff_land.
       apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos.
       rewrite Z.testbit_0_l, Z.land_spec, Z.lnot_spec, Z.lor_spec;
@@ -1240,7 +1240,7 @@ Module Z.
         -> (y <= z)%Z
         -> (Z.lor x y <= (2 ^ Z.log2_up (z+1)) - 1)%Z.
     Proof.
-      intros; apply Z.ldiff_le.
+      intros x y z H H0 H1; apply Z.ldiff_le.
 
       - apply Z.le_add_le_sub_r.
         replace 1%Z with (2 ^ 0)%Z by (cbv; reflexivity).
@@ -1538,7 +1538,7 @@ Module N2Z.
 
   Lemma inj_shiftl: forall x y, Z.of_N (N.shiftl x y) = Z.shiftl (Z.of_N x) (Z.of_N y).
   Proof.
-    intros.
+    intros x y.
     apply Z.bits_inj_iff'; intros k Hpos.
     rewrite Z2N.inj_testbit; [|assumption].
     rewrite Z.shiftl_spec; [|assumption].
diff --git a/src/Util/ZUtil/Land.v b/src/Util/ZUtil/Land.v
index b3d3f3727..f46d541e9 100644
--- a/src/Util/ZUtil/Land.v
+++ b/src/Util/ZUtil/Land.v
@@ -5,7 +5,7 @@ Local Open Scope Z_scope.
 Module Z.
   Lemma land_same_r : forall a b, (a &' b) &' b = a &' b.
   Proof.
-    intros; apply Z.bits_inj'; intros.
+    intros a b; apply Z.bits_inj'; intros n H.
     rewrite !Z.land_spec.
     case_eq (Z.testbit b n); intros;
       rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; reflexivity.
diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v
index 511898b48..4e14907e8 100644
--- a/src/Util/ZUtil/Modulo.v
+++ b/src/Util/ZUtil/Modulo.v
@@ -14,38 +14,38 @@ Module Z.
   Hint Resolve elim_mod : zarith.
 
   Lemma mod_add_full : forall a b c, (a + b * c) mod c = a mod c.
-  Proof. intros; destruct (Z_zerop c); try subst; autorewrite with zsimplify; reflexivity. Qed.
+  Proof. intros a b c; destruct (Z_zerop c); try subst; autorewrite with zsimplify; reflexivity. Qed.
   Hint Rewrite mod_add_full : zsimplify.
 
   Lemma mod_add_l_full : forall a b c, (a * b + c) mod b = c mod b.
-  Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
+  Proof. intros a b c; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
   Hint Rewrite mod_add_l_full : zsimplify.
 
   Lemma mod_add'_full : forall a b c, (a + b * c) mod b = a mod b.
-  Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
+  Proof. intros a b c; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
   Lemma mod_add_l'_full : forall a b c, (a * b + c) mod a = c mod a.
-  Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed.
+  Proof. intros a b c; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed.
   Hint Rewrite mod_add'_full mod_add_l'_full : zsimplify.
 
   Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b.
-  Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
+  Proof. intros a b c H; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
 
   Lemma mod_add' : forall a b c, b <> 0 -> (a + b * c) mod b = a mod b.
-  Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
+  Proof. intros a b c H; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
   Lemma mod_add_l' : forall a b c, a <> 0 -> (a * b + c) mod a = c mod a.
-  Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed.
+  Proof. intros a b c H; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed.
 
   Lemma add_pow_mod_l : forall a b c, a <> 0 -> 0 < b ->
                                       ((a ^ b) + c) mod a = c mod a.
   Proof.
-    intros; replace b with (b - 1 + 1) by ring;
+    intros a b c H H0; replace b with (b - 1 + 1) by ring;
       rewrite Z.pow_add_r, Z.pow_1_r by omega; auto using Z.mod_add_l.
   Qed.
 
   Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 ->
     a ^ x mod m = 0.
   Proof.
-    intros.
+    intros a x m H H0 H1.
     replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega).
     induction (Z.to_nat x). {
       simpl in *; omega.
@@ -70,8 +70,8 @@ Module Z.
   Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) ->
       a ^ b mod m = (a mod m) ^ b mod m.
   Proof.
-    intros; rewrite <- (Z2Nat.id b) by auto.
-    induction (Z.to_nat b); auto.
+    intros a m b H H0; rewrite <- (Z2Nat.id b) by auto.
+    induction (Z.to_nat b) as [|n IHn]; auto.
     rewrite Nat2Z.inj_succ.
     do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg.
     rewrite Z.mul_mod by auto.
@@ -90,7 +90,7 @@ Module Z.
 
   Lemma mul_div_eq_full : forall a m, m <> 0 -> m * (a / m) = (a - a mod m).
   Proof.
-    intros. rewrite (Z_div_mod_eq_full a m) at 2 by auto. ring.
+    intros a m H. rewrite (Z_div_mod_eq_full a m) at 2 by auto. ring.
   Qed.
 
   Hint Rewrite mul_div_eq_full using zutil_arith : zdiv_to_mod.
@@ -126,14 +126,14 @@ Module Z.
 
   Lemma mul_div_eq : forall a m, m > 0 -> m * (a / m) = (a - a mod m).
   Proof.
-    intros.
+    intros a m H.
     rewrite (Z_div_mod_eq a m) at 2 by auto.
     ring.
   Qed.
 
   Lemma mul_div_eq' : (forall a m, m > 0 -> (a / m) * m = (a - a mod m))%Z.
   Proof.
-    intros.
+    intros a m H.
     rewrite (Z_div_mod_eq a m) at 2 by auto.
     ring.
   Qed.
diff --git a/src/Util/ZUtil/Testbit.v b/src/Util/ZUtil/Testbit.v
index a315f7e4b..175d07b02 100644
--- a/src/Util/ZUtil/Testbit.v
+++ b/src/Util/ZUtil/Testbit.v
@@ -22,7 +22,7 @@ Module Z.
                                             then true
                                             else if Z_lt_dec m n then true else false.
   Proof.
-    intros.
+    intros n m.
     repeat (break_match || autorewrite with Ztestbit); try reflexivity; try omega.
     unfold Z.ones.
     rewrite <- Z.shiftr_opp_r, Z.shiftr_eq_0 by (simpl; omega); simpl.
@@ -34,7 +34,7 @@ Module Z.
   Lemma testbit_pow2_mod : forall a n i, 0 <= n ->
   Z.testbit (Z.pow2_mod a n) i = if Z_lt_dec i n then Z.testbit a i else false.
   Proof.
-  cbv [Z.pow2_mod]; intros; destruct (Z_le_dec 0 i);
+    cbv [Z.pow2_mod]; intros a n i H; destruct (Z_le_dec 0 i);
       repeat match goal with
           | |- _ => rewrite Z.testbit_neg_r by omega
           | |- _ => break_innermost_match_step
@@ -50,7 +50,7 @@ Module Z.
                                      then if Z_lt_dec i 0 then false else Z.testbit a i
                                      else if Z_lt_dec i n then Z.testbit a i else false.
   Proof.
-    intros; destruct (Z_lt_dec n 0); [ | apply testbit_pow2_mod; omega ].
+    intros a n i; destruct (Z_lt_dec n 0); [ | apply testbit_pow2_mod; omega ].
     unfold Z.pow2_mod.
     autorewrite with Ztestbit_full;
       repeat break_match;
@@ -80,7 +80,7 @@ Module Z.
   Lemma testbit_add_shiftl_low : forall i, (0 <= i) -> forall a b n, (i < n) ->
     Z.testbit (a + Z.shiftl b n) i = Z.testbit a i.
   Proof.
-    intros.
+    intros i H a b n H0.
     erewrite Z.testbit_low; eauto.
     rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega.
     rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega).