Merge PR #13173: Lint stdlib with -mangle-names #4

Reviewed-by: anton-trunov

10 files changed, 119 insertions, 116 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 9a30e011af..52998c8b95 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -126,7 +126,7 @@ Lemma pos_sub_spec p q :
    | Gt => pos (p - q)
  end.
 Proof.
- revert q. induction p; destruct q; simpl; trivial;
+ revert q. induction p as [p IHp|p IHp|]; intros q; destruct q; simpl; trivial;
  rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI,
   ?Pos.compare_xI_xO, ?Pos.compare_xO_xO, IHp; simpl;
  case Pos.compare_spec; intros; simpl; trivial;
@@ -168,7 +168,7 @@ Qed.
 
 Lemma pos_sub_opp p q : - pos_sub p q = pos_sub q p.
 Proof.
- revert q; induction p; destruct q; simpl; trivial;
+ revert q; induction p as [p IHp|p IHp|]; intros q; destruct q; simpl; trivial;
  rewrite <- IHp; now destruct pos_sub.
 Qed.
 
@@ -468,13 +468,13 @@ Lemma peano_ind (P : Z -> Prop) :
   (forall x, P x -> P (pred x)) ->
   forall z, P z.
 Proof.
- intros H0 Hs Hp z; destruct z.
+ intros H0 Hs Hp z; destruct z as [|p|p].
  assumption.
- induction p using Pos.peano_ind.
+ induction p as [|p IHp] using Pos.peano_ind.
   now apply (Hs 0).
   rewrite <- Pos.add_1_r.
   now apply (Hs (pos p)).
- induction p using Pos.peano_ind.
+ induction p as [|p IHp] using Pos.peano_ind.
   now apply (Hp 0).
   rewrite <- Pos.add_1_r.
   now apply (Hp (neg p)).
@@ -486,7 +486,7 @@ Lemma bi_induction (P : Z -> Prop) :
   (forall x, P x <-> P (succ x)) ->
   forall z, P z.
 Proof.
- intros _ H0 Hs. induction z using peano_ind.
+ intros _ H0 Hs z. induction z using peano_ind.
  assumption.
  now apply -> Hs.
  apply Hs. now rewrite succ_pred.
@@ -569,7 +569,7 @@ Qed.
 Lemma sqrtrem_spec n : 0<=n ->
  let (s,r) := sqrtrem n in n = s*s + r /\ 0 <= r <= 2*s.
 Proof.
- destruct n. now repeat split.
+ destruct n as [|p|p]. now repeat split.
  generalize (Pos.sqrtrem_spec p). simpl.
  destruct 1; simpl; subst; now repeat split.
  now destruct 1.
@@ -578,7 +578,7 @@ Qed.
 Lemma sqrt_spec n : 0<=n ->
  let s := sqrt n in s*s <= n < (succ s)*(succ s).
 Proof.
- destruct n. now repeat split. unfold sqrt.
+ destruct n as [|p|p]. now repeat split. unfold sqrt.
  intros _. simpl succ. rewrite Pos.add_1_r. apply (Pos.sqrt_spec p).
  now destruct 1.
 Qed.
@@ -590,7 +590,7 @@ Qed.
 
 Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n.
 Proof.
- destruct n; try reflexivity.
+ destruct n as [|p|p]; try reflexivity.
  unfold sqrtrem, sqrt, Pos.sqrt.
  destruct (Pos.sqrtrem p) as (s,r). now destruct r.
 Qed.
@@ -655,7 +655,7 @@ Lemma pos_div_eucl_eq a b : 0 < b ->
   let (q, r) := pos_div_eucl a b in pos a = q * b + r.
 Proof.
  intros Hb.
- induction a; unfold pos_div_eucl; fold pos_div_eucl.
+ induction a as [a IHa|a IHa|]; unfold pos_div_eucl; fold pos_div_eucl.
  - (* ~1 *)
    destruct pos_div_eucl as (q,r).
    change (pos a~1) with (2*(pos a)+1).
@@ -720,7 +720,7 @@ Proof.
   now rewrite Pos.add_diag.
  intros Hb.
  destruct b as [|b|b]; discriminate Hb || clear Hb.
- induction a; unfold pos_div_eucl; fold pos_div_eucl.
+ induction a as [a IHa|a IHa|]; unfold pos_div_eucl; fold pos_div_eucl.
  (* ~1 *)
  destruct pos_div_eucl as (q,r).
  simpl in IHa; destruct IHa as (Hr,Hr').
@@ -996,7 +996,7 @@ Proof.
  intros Hn Hm. unfold shiftr.
  destruct n as [ |n|n]; (now destruct Hn) || clear Hn; simpl.
  now rewrite add_0_r.
- assert (forall p, to_N (m + pos p) = (to_N m + N.pos p)%N).
+ assert (forall p, to_N (m + pos p) = (to_N m + N.pos p)%N) as H.
   destruct m; trivial; now destruct Hm.
  assert (forall p, 0 <= m + pos p).
   destruct m; easy || now destruct Hm.
@@ -1054,7 +1054,7 @@ Proof.
   subst. now rewrite N.sub_diag.
   simpl. destruct (Pos.sub_mask_pos' m n H') as (p & -> & <-).
   f_equal. now rewrite Pos.add_comm, Pos.add_sub.
- destruct a; unfold shiftl.
+ destruct a as [|p|p]; unfold shiftl.
  (* ... a = 0 *)
  replace (Pos.iter (mul 2) 0 n) with 0
   by (apply Pos.iter_invariant; intros; subst; trivial).
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 62fccf3ce2..9fa05dd2f7 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -67,7 +67,7 @@ Lemma natlike_ind :
    forall x:Z, 0 <= x -> P x.
 Proof.
  intros P Ho Hrec x Hx; apply Z_of_nat_prop; trivial.
- induction n. exact Ho.
+ intros n; induction n. exact Ho.
  rewrite Nat2Z.inj_succ. apply Hrec; trivial using Nat2Z.is_nonneg.
 Qed.
 
@@ -78,7 +78,7 @@ Lemma natlike_rec :
    forall x:Z, 0 <= x -> P x.
 Proof.
  intros P Ho Hrec x Hx; apply Z_of_nat_set; trivial.
- induction n. exact Ho.
+ intros n; induction n. exact Ho.
  rewrite Nat2Z.inj_succ. apply Hrec; trivial using Nat2Z.is_nonneg.
 Qed.
 
@@ -101,9 +101,9 @@ Section Efficient_Rec.
       (forall z:Z, 0 <= z -> P z -> P (Z.succ z)) ->
       forall z:Z, 0 <= z -> P z.
   Proof.
-   intros P Ho Hrec.
+   intros P Ho Hrec z.
    induction z as [z IH] using (well_founded_induction_type R_wf).
-   destruct z; intros Hz.
+   destruct z as [|p|p]; intros Hz.
    - apply Ho.
    - set (y:=Z.pred (Zpos p)).
      assert (LE : 0 <= y) by (unfold y; now apply Z.lt_le_pred).
@@ -121,9 +121,9 @@ Section Efficient_Rec.
       (forall z:Z, 0 < z -> P (Z.pred z) -> P z) ->
       forall z:Z, 0 <= z -> P z.
   Proof.
-   intros P Ho Hrec.
+   intros P Ho Hrec z.
    induction z as [z IH] using (well_founded_induction_type R_wf).
-   destruct z; intros Hz.
+   destruct z as [|p|p]; intros Hz.
    - apply Ho.
    - assert (EQ : 0 <= Z.pred (Zpos p)) by now apply Z.lt_le_pred.
      apply Hrec. easy. apply IH; trivial. split; trivial.
@@ -138,7 +138,7 @@ Section Efficient_Rec.
       (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> 0 <= x -> P x) ->
       forall x:Z, 0 <= x -> P x.
   Proof.
-   intros P Hrec.
+   intros P Hrec x.
    induction x as [x IH] using (well_founded_induction_type R_wf).
    destruct x; intros Hx.
    - apply Hrec; trivial. intros y (Hy,Hy').
@@ -196,7 +196,7 @@ Section Efficient_Rec.
       (forall x:Z, (forall y:Z, z <= y < x -> P y) -> z <= x -> P x) ->
       forall x:Z, z <= x -> P x.
   Proof.
-    intros; now apply Zlt_lower_bound_rec with z.
+    intros P z ? x ?; now apply Zlt_lower_bound_rec with z.
   Qed.
 
 End Efficient_Rec.
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index 834f16cd9e..dc40f9ea51 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -19,7 +19,7 @@ Local Open Scope Z_scope.
 (* Trivial, to deprecate? *)
 Lemma Dcompare_inf : forall r:comparison, {r = Eq} + {r = Lt} + {r = Gt}.
 Proof.
-  induction r; auto.
+  intros r; induction r; auto.
 Defined.
 (* end hide *)
 
@@ -92,7 +92,7 @@ Section decidability.
   Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}.
   Proof.
     intro H.
-    apply Zcompare_rec with (n := x) (m := y).
+    apply (Zcompare_rec _ x y).
     intro. right. elim (Z.compare_eq_iff x y); auto with arith.
     intro. left. elim (Z.compare_eq_iff x y); auto with arith.
     intro H1. absurd (x > y); auto with arith.
@@ -111,7 +111,7 @@ Proof.
   assumption.
   intro.
   right.
-  apply Z.le_lt_trans with (m := x).
+  apply (Z.le_lt_trans _ x).
   apply Z.ge_le.
   assumption.
   assumption.
@@ -123,14 +123,14 @@ Proof.
   case (Zlt_cotrans 0 (x + y) H x).
   - now left.
   - right.
-    apply Z.add_lt_mono_l with (p := x).
+    apply (Z.add_lt_mono_l _ _ x).
     now rewrite Z.add_0_r.
 Defined.
 
 Lemma Zlt_cotrans_neg : forall n m:Z, n + m < 0 -> {n < 0} + {m < 0}.
 Proof.
   intros x y H; case (Zlt_cotrans (x + y) 0 H x); intro Hxy;
-    [ right; apply Z.add_lt_mono_l with (p := x); rewrite Z.add_0_r | left ];
+    [ right; apply (Z.add_lt_mono_l _ _ x); rewrite Z.add_0_r | left ];
     assumption.
 Defined.
 
@@ -143,7 +143,7 @@ Proof.
   assumption.
   intro H0.
   generalize (Z.ge_le _ _ H0).
-  intro.
+  intro H1.
   case (Z_le_lt_eq_dec _ _ H1).
   intro.
   right.
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 21086d9b61..f869e15023 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -49,12 +49,12 @@ Qed.
 
 Theorem Zabs_intro : forall P (n:Z), P (- n) -> P n -> P (Z.abs n).
 Proof.
- now destruct n.
+ intros P n; now destruct n.
 Qed.
 
 Definition Zabs_dec : forall x:Z, {x = Z.abs x} + {x = - Z.abs x}.
 Proof.
- destruct x; auto.
+ intros x; destruct x; auto.
 Defined.
 
 Lemma Zabs_spec x :
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index c9e1b340a6..c848623d06 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -13,7 +13,6 @@ Require Import ZArith_base.
 Require Import Wf_nat.
 Local Open Scope Z_scope.
 
-
 (**********************************************************************)
 (** About parity *)
 
@@ -39,7 +38,7 @@ Proof. reflexivity. Qed.
 
 Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p.
 Proof.
- unfold floor. induction p as [p [IH1p IH2p]|p [IH1p IH2]|]; simpl.
+ unfold floor. intros p; induction p as [p [IH1p IH2p]|p [IH1p IH2]|]; simpl.
  - rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO.
    split.
    + apply Z.le_trans with (2 * Z.pos p); auto with zarith.
@@ -69,10 +68,10 @@ Proof.
   apply (Z_lt_rec Q); auto with zarith.
   subst Q; intros x H.
   split; apply HP.
-  - rewrite Z.abs_eq; auto; intros.
+  - rewrite Z.abs_eq; auto; intros m ?.
     destruct (H (Z.abs m)); auto with zarith.
     destruct (Zabs_dec m) as [-> | ->]; trivial.
-  - rewrite Z.abs_neq, Z.opp_involutive; intros.
+  - rewrite Z.abs_neq, Z.opp_involutive; [intros m ?|].
     + destruct (H (Z.abs m)); auto with zarith.
       destruct (Zabs_dec m) as [-> | ->]; trivial.
     + apply Z.opp_le_mono; rewrite Z.opp_involutive; auto.
@@ -85,15 +84,15 @@ Theorem Z_lt_abs_induction :
 Proof.
   intros P HP p.
   set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *.
-  enough (Q (Z.abs p)) by
+  enough (Q (Z.abs p)) as H by
     (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).
   apply (Z_lt_induction Q); auto with zarith.
-  subst Q; intros.
+  subst Q; intros ? H.
   split; apply HP.
-  - rewrite Z.abs_eq; auto; intros.
+  - rewrite Z.abs_eq; auto; intros m ?.
     elim (H (Z.abs m)); intros; auto with zarith.
     elim (Zabs_dec m); intro eq; rewrite eq; trivial.
-  - rewrite Z.abs_neq, Z.opp_involutive; intros.
+  - rewrite Z.abs_neq, Z.opp_involutive; [intros m ?|].
     + destruct (H (Z.abs m)); auto with zarith.
       destruct (Zabs_dec m) as [-> | ->]; trivial.
     + apply Z.opp_le_mono; rewrite Z.opp_involutive; auto.
@@ -136,7 +135,7 @@ Section Zlength_properties.
   Lemma Zlength_correct l : Zlength l = Z.of_nat (length l).
   Proof.
     assert (H : forall l acc, Zlength_aux acc A l = acc + Z.of_nat (length l)).
-    clear l. induction l.
+    clear l. intros l; induction l as [|? ? IHl].
     auto with zarith.
     intros. simpl length; simpl Zlength_aux.
      rewrite IHl, Nat2Z.inj_succ, Z.add_succ_comm; auto.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index b6fbe64499..2039dc0bee 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -174,22 +174,22 @@ Proof. intros; eapply Zmod_unique_full; eauto. Qed.
 
 Lemma Zmod_0_l: forall a, 0 mod a = 0.
 Proof.
-  destruct a; simpl; auto.
+  intros a; destruct a; simpl; auto.
 Qed.
 
 Lemma Zmod_0_r: forall a, a mod 0 = 0.
 Proof.
-  destruct a; simpl; auto.
+  intros a; destruct a; simpl; auto.
 Qed.
 
 Lemma Zdiv_0_l: forall a, 0/a = 0.
 Proof.
-  destruct a; simpl; auto.
+  intros a; destruct a; simpl; auto.
 Qed.
 
 Lemma Zdiv_0_r: forall a, a/0 = 0.
 Proof.
-  destruct a; simpl; auto.
+  intros a; destruct a; simpl; auto.
 Qed.
 
 Ltac zero_or_not a :=
@@ -198,10 +198,10 @@ Ltac zero_or_not a :=
    auto with zarith|].
 
 Lemma Zmod_1_r: forall a, a mod 1 = 0.
-Proof. intros. zero_or_not a. apply Z.mod_1_r. Qed.
+Proof. intros a. zero_or_not a. apply Z.mod_1_r. Qed.
 
 Lemma Zdiv_1_r: forall a, a/1 = a.
-Proof. intros. zero_or_not a. apply Z.div_1_r. Qed.
+Proof. intros a. zero_or_not a. apply Z.div_1_r. Qed.
 
 Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r
  : zarith.
@@ -216,10 +216,10 @@ Lemma Z_div_same_full : forall a:Z, a<>0 -> a/a = 1.
 Proof Z.div_same.
 
 Lemma Z_mod_same_full : forall a, a mod a = 0.
-Proof. intros. zero_or_not a. apply Z.mod_same; auto. Qed.
+Proof. intros a. zero_or_not a. apply Z.mod_same; auto. Qed.
 
 Lemma Z_mod_mult : forall a b, (a*b) mod b = 0.
-Proof. intros. zero_or_not b. apply Z.mod_mul. auto. Qed.
+Proof. intros a b. zero_or_not b. apply Z.mod_mul. auto. Qed.
 
 Lemma Z_div_mult_full : forall a b:Z, b <> 0 -> (a*b)/b = a.
 Proof Z.div_mul.
@@ -313,7 +313,7 @@ Proof. intros; apply Z.div_le_compat_l; intuition auto using Z.lt_le_incl. Qed.
 Theorem Zdiv_sgn: forall a b,
   0 <= Z.sgn (a/b) * Z.sgn a * Z.sgn b.
 Proof.
-  destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith;
+  intros a b; destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith;
   generalize (Z.div_pos (Zpos a) (Zpos b)); unfold Z.div, Z.div_eucl;
   destruct Z.pos_div_eucl as (q,r); destruct r;
   rewrite ?Z.mul_1_r, <-?Z.opp_eq_mul_m1, ?Z.sgn_opp, ?Z.opp_involutive;
@@ -325,7 +325,7 @@ Qed.
 (** * Relations between usual operations and Z.modulo and Z.div *)
 
 Lemma Z_mod_plus_full : forall a b c:Z, (a + b * c) mod c = a mod c.
-Proof. intros. zero_or_not c. apply Z.mod_add; auto. Qed.
+Proof. intros a b c. zero_or_not c. apply Z.mod_add; auto. Qed.
 
 Lemma Z_div_plus_full : forall a b c:Z, c <> 0 -> (a + b * c) / c = a / c + b.
 Proof Z.div_add.
@@ -338,34 +338,34 @@ Proof Z.div_add_l.
     some of the relations about [Z.opp] and divisions are rather complex. *)
 
 Lemma Zdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b.
-Proof. intros. zero_or_not b. apply Z.div_opp_opp; auto. Qed.
+Proof. intros a b. zero_or_not b. apply Z.div_opp_opp; auto. Qed.
 
 Lemma Zmod_opp_opp : forall a b:Z, (-a) mod (-b) = - (a mod b).
-Proof. intros. zero_or_not b. apply Z.mod_opp_opp; auto. Qed.
+Proof. intros a b. zero_or_not b. apply Z.mod_opp_opp; auto. Qed.
 
 Lemma Z_mod_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a) mod b = 0.
-Proof. intros. zero_or_not b. apply Z.mod_opp_l_z; auto. Qed.
+Proof. intros a b. zero_or_not b. apply Z.mod_opp_l_z; auto. Qed.
 
 Lemma Z_mod_nz_opp_full : forall a b:Z, a mod b <> 0 ->
  (-a) mod b = b - (a mod b).
-Proof. intros. zero_or_not b. apply Z.mod_opp_l_nz; auto. Qed.
+Proof. intros a b. zero_or_not b. apply Z.mod_opp_l_nz; auto. Qed.
 
 Lemma Z_mod_zero_opp_r : forall a b:Z, a mod b = 0 -> a mod (-b) = 0.
-Proof. intros. zero_or_not b. apply Z.mod_opp_r_z; auto. Qed.
+Proof. intros a b. zero_or_not b. apply Z.mod_opp_r_z; auto. Qed.
 
 Lemma Z_mod_nz_opp_r : forall a b:Z, a mod b <> 0 ->
  a mod (-b) = (a mod b) - b.
-Proof. intros. zero_or_not b. apply Z.mod_opp_r_nz; auto. Qed.
+Proof. intros a b ?. zero_or_not b. apply Z.mod_opp_r_nz; auto. Qed.
 
 Lemma Z_div_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a)/b = -(a/b).
-Proof. intros. zero_or_not b. apply Z.div_opp_l_z; auto. Qed.
+Proof. intros a b ?. zero_or_not b. apply Z.div_opp_l_z; auto. Qed.
 
 Lemma Z_div_nz_opp_full : forall a b:Z, a mod b <> 0 ->
  (-a)/b = -(a/b)-1.
 Proof. intros a b. zero_or_not b. easy. intros; rewrite Z.div_opp_l_nz; auto. Qed.
 
 Lemma Z_div_zero_opp_r : forall a b:Z, a mod b = 0 -> a/(-b) = -(a/b).
-Proof. intros. zero_or_not b. apply Z.div_opp_r_z; auto. Qed.
+Proof. intros a b ?. zero_or_not b. apply Z.div_opp_r_z; auto. Qed.
 
 Lemma Z_div_nz_opp_r : forall a b:Z, a mod b <> 0 ->
  a/(-b) = -(a/b)-1.
@@ -375,19 +375,19 @@ Proof. intros a b. zero_or_not b. easy. intros; rewrite Z.div_opp_r_nz; auto. Qe
 
 Lemma  Zdiv_mult_cancel_r : forall a b c:Z,
  c <> 0 -> (a*c)/(b*c) = a/b.
-Proof. intros. zero_or_not b. apply Z.div_mul_cancel_r; auto. Qed.
+Proof. intros a b c ?. zero_or_not b. apply Z.div_mul_cancel_r; auto. Qed.
 
 Lemma Zdiv_mult_cancel_l : forall a b c:Z,
  c<>0 -> (c*a)/(c*b) = a/b.
 Proof.
- intros. rewrite (Z.mul_comm c b); zero_or_not b.
+ intros a b c ?. rewrite (Z.mul_comm c b); zero_or_not b.
  rewrite (Z.mul_comm b c). apply Z.div_mul_cancel_l; auto.
 Qed.
 
 Lemma Zmult_mod_distr_l: forall a b c,
   (c*a) mod (c*b) = c * (a mod b).
 Proof.
- intros. zero_or_not c. rewrite (Z.mul_comm c b); zero_or_not b.
+ intros a b c. zero_or_not c. rewrite (Z.mul_comm c b); zero_or_not b.
  + now rewrite Z.mul_0_r.
  + rewrite (Z.mul_comm b c). apply Z.mul_mod_distr_l; auto.
 Qed.
@@ -395,7 +395,7 @@ Qed.
 Lemma Zmult_mod_distr_r: forall a b c,
   (a*c) mod (b*c) = (a mod b) * c.
 Proof.
- intros. zero_or_not b. rewrite (Z.mul_comm b c); zero_or_not c.
+ intros a b c. zero_or_not b. rewrite (Z.mul_comm b c); zero_or_not c.
  + now rewrite Z.mul_0_r.
  + rewrite (Z.mul_comm c b). apply Z.mul_mod_distr_r; auto.
 Qed.
@@ -403,27 +403,27 @@ Qed.
 (** Operations modulo. *)
 
 Theorem Zmod_mod: forall a n, (a mod n) mod n = a mod n.
-Proof. intros. zero_or_not n. apply Z.mod_mod; auto. Qed.
+Proof. intros a n. zero_or_not n. apply Z.mod_mod; auto. Qed.
 
 Theorem Zmult_mod: forall a b n,
  (a * b) mod n = ((a mod n) * (b mod n)) mod n.
-Proof. intros. zero_or_not n. apply Z.mul_mod; auto. Qed.
+Proof. intros a b n. zero_or_not n. apply Z.mul_mod; auto. Qed.
 
 Theorem Zplus_mod: forall a b n,
  (a + b) mod n = (a mod n + b mod n) mod n.
-Proof. intros. zero_or_not n. apply Z.add_mod; auto. Qed.
+Proof. intros a b n. zero_or_not n. apply Z.add_mod; auto. Qed.
 
 Theorem Zminus_mod: forall a b n,
  (a - b) mod n = (a mod n - b mod n) mod n.
 Proof.
-  intros.
+  intros a b n.
   replace (a - b) with (a + (-1) * b); auto with zarith.
   replace (a mod n - b mod n) with (a mod n + (-1) * (b mod n)); auto with zarith.
   rewrite Zplus_mod.
   rewrite Zmult_mod.
-  rewrite Zplus_mod with (b:=(-1) * (b mod n)).
+  rewrite (Zplus_mod _ ((-1) * (b mod n))).
   rewrite Zmult_mod.
-  rewrite Zmult_mod with (b:= b mod n).
+  rewrite (Zmult_mod _ (b mod n)).
   repeat rewrite Zmod_mod; auto.
 Qed.
 
@@ -483,17 +483,20 @@ Qed.
 
 Instance Zplus_eqm : Proper (eqm ==> eqm ==> eqm) Z.add.
 Proof.
-  unfold eqm; repeat red; intros. rewrite Zplus_mod, H, H0, <- Zplus_mod; auto.
+  unfold eqm; repeat red; intros ? ? H ? ? H0.
+  rewrite Zplus_mod, H, H0, <- Zplus_mod; auto.
 Qed.
 
 Instance Zminus_eqm : Proper (eqm ==> eqm ==> eqm) Z.sub.
 Proof.
-  unfold eqm; repeat red; intros. rewrite Zminus_mod, H, H0, <- Zminus_mod; auto.
+  unfold eqm; repeat red; intros ? ? H ? ? H0.
+  rewrite Zminus_mod, H, H0, <- Zminus_mod; auto.
 Qed.
 
 Instance Zmult_eqm : Proper (eqm ==> eqm ==> eqm) Z.mul.
 Proof.
-  unfold eqm; repeat red; intros. rewrite Zmult_mod, H, H0, <- Zmult_mod; auto.
+  unfold eqm; repeat red; intros ? ? H ? ? H0.
+  rewrite Zmult_mod, H, H0, <- Zmult_mod; auto.
 Qed.
 
 Instance Zopp_eqm : Proper (eqm ==> eqm) Z.opp.
@@ -503,7 +506,7 @@ Qed.
 
 Lemma Zmod_eqm : forall a, (a mod N) == a.
 Proof.
-  intros; exact (Zmod_mod a N).
+  intros a; exact (Zmod_mod a N).
 Qed.
 
 (* NB: Z.modulo and Z.div are not morphisms with respect to eqm.
@@ -518,7 +521,7 @@ End EqualityModulo.
 
 Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c).
 Proof.
- intros. zero_or_not b. rewrite Z.mul_comm. zero_or_not c.
+ intros a b c ? ?. zero_or_not b. rewrite Z.mul_comm. zero_or_not c.
  rewrite Z.mul_comm. apply Z.div_div; auto.
  apply Z.le_neq; auto.
 Qed.
@@ -538,7 +541,7 @@ Qed.
 Theorem Zdiv_mult_le:
  forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b.
 Proof.
- intros. zero_or_not b. now rewrite Z.mul_0_r.
+ intros a b c ? ? ?. zero_or_not b. now rewrite Z.mul_0_r.
  apply Z.div_mul_le; auto.
  apply Z.le_neq; auto.
 Qed.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 6a82645ba6..7f72d42d1f 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -50,7 +50,7 @@ Qed.
 
 Lemma N_nat_Z n : Z.of_nat (N.to_nat n) = Z.of_N n.
 Proof.
- destruct n; trivial. simpl.
+ destruct n as [|p]; trivial. simpl.
  destruct (Pos2Nat.is_succ p) as (m,H).
  rewrite H. simpl. f_equal. now apply SuccNat2Pos.inv.
 Qed.
@@ -668,7 +668,7 @@ Qed.
 
 Lemma inj_abs_nat z : Z.of_nat (Z.abs_nat z) = Z.abs z.
 Proof.
- destruct z; simpl; trivial;
+ destruct z as [|p|p]; simpl; trivial;
   destruct (Pos2Nat.is_succ p) as (n,H); rewrite H; simpl; f_equal;
    now apply SuccNat2Pos.inv.
 Qed.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 6ba58df721..cad9454906 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -256,15 +256,15 @@ Qed.
 Lemma Zis_gcd_for_euclid :
   forall a b d q:Z, Zis_gcd b (a - q * b) d -> Zis_gcd a b d.
 Proof.
-  simple induction 1; constructor; intuition.
+  intros a b d q; simple induction 1; constructor; intuition.
   replace a with (a - q * b + q * b). auto with zarith. ring.
 Qed.
 
 Lemma Zis_gcd_for_euclid2 :
   forall b d q r:Z, Zis_gcd r b d -> Zis_gcd b (b * q + r) d.
 Proof.
-  simple induction 1; constructor; intuition.
-  apply H2; auto.
+  intros b d q r; destruct 1 as [? ? H]; constructor; intuition.
+  apply H; auto.
   replace r with (b * q + r - b * q). auto with zarith. ring.
 Qed.
 
@@ -300,9 +300,9 @@ Section extended_euclid_algorithm.
   Proof.
     intros v3 Hv3; generalize Hv3; pattern v3.
     apply Zlt_0_rec.
-    clear v3 Hv3; intros.
+    clear v3 Hv3; intros x H ? ? u1 u2 u3 v1 v2 H1 H2 H3.
     destruct (Z_zerop x) as [Heq|Hneq].
-    apply Euclid_intro with (u := u1) (v := u2) (d := u3).
+    apply (Euclid_intro u1 u2 u3).
     assumption.
     apply H3.
     rewrite Heq; auto with zarith.
@@ -333,12 +333,10 @@ Section extended_euclid_algorithm.
   Proof.
     case (Z_le_gt_dec 0 b); intro.
     intros;
-      apply euclid_rec with
-	(u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := 1) (v3 := b);
+      apply (fun H => euclid_rec b H 1 0 a 0 1);
       auto; ring.
     intros;
-      apply euclid_rec with
-	(u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := -1) (v3 := - b);
+      apply (fun H => euclid_rec (- b) H 1 0 a 0 (-1));
       auto; try ring.
     now apply Z.opp_nonneg_nonpos, Z.lt_le_incl, Z.gt_lt.
     auto with zarith.
@@ -349,8 +347,8 @@ End extended_euclid_algorithm.
 Theorem Zis_gcd_uniqueness_apart_sign :
   forall a b d d':Z, Zis_gcd a b d -> Zis_gcd a b d' -> d = d' \/ d = - d'.
 Proof.
-  simple induction 1.
-  intros H1 H2 H3; simple induction 1; intros.
+  intros a b d d'; simple induction 1.
+  intros H1 H2 H3; destruct 1 as [H4 H5 H6].
   generalize (H3 d' H4 H5); intro Hd'd.
   generalize (H6 d H1 H2); intro Hdd'.
   exact (Z.divide_antisym d d' Hdd' Hd'd).
@@ -368,7 +366,7 @@ Proof.
   intros a b d Hgcd.
   elim (euclid a b); intros u v d0 e g.
   generalize (Zis_gcd_uniqueness_apart_sign a b d d0 Hgcd g).
-  intro H; elim H; clear H; intros.
+  intro H; elim H; clear H; intros H.
   apply Bezout_intro with u v.
   rewrite H; assumption.
   apply Bezout_intro with (- u) (- v).
@@ -380,7 +378,7 @@ Qed.
 Lemma Zis_gcd_mult :
   forall a b c d:Z, Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d).
 Proof.
-  intros a b c d; simple induction 1. constructor; auto with zarith.
+  intros a b c d; intro H; generalize H; simple induction 1. constructor; auto with zarith.
   intros x Ha Hb.
   elim (Zis_gcd_bezout a b d H). intros u v Huv.
   elim Ha; intros a' Ha'.
@@ -407,7 +405,7 @@ Qed.
 
 Lemma bezout_rel_prime : forall a b:Z, Bezout a b 1 -> rel_prime a b.
 Proof.
-  simple induction 1; constructor; auto with zarith.
+  simple induction 1; intros ? ? H0; constructor; auto with zarith.
   intros. rewrite <- H0; auto with zarith.
 Qed.
 
@@ -416,7 +414,7 @@ Qed.
 
 Theorem Gauss : forall a b c:Z, (a | b * c) -> rel_prime a b -> (a | c).
 Proof.
-  intros. elim (rel_prime_bezout a b H0); intros.
+  intros a b c H H0. elim (rel_prime_bezout a b H0); intros u v H1.
   replace c with (c * 1); [ idtac | ring ].
   rewrite <- H1.
   replace (c * (u * a + v * b)) with (c * u * a + v * (b * c));
@@ -429,11 +427,11 @@ Lemma rel_prime_mult :
   forall a b c:Z, rel_prime a b -> rel_prime a c -> rel_prime a (b * c).
 Proof.
   intros a b c Hb Hc.
-  elim (rel_prime_bezout a b Hb); intros.
-  elim (rel_prime_bezout a c Hc); intros.
+  elim (rel_prime_bezout a b Hb); intros u v H.
+  elim (rel_prime_bezout a c Hc); intros u0 v0 H0.
   apply bezout_rel_prime.
-  apply Bezout_intro with
-    (u := u * u0 * a + v0 * c * u + u0 * v * b) (v := v * v0).
+  apply (Bezout_intro _ _ _
+    (u * u0 * a + v0 * c * u + u0 * v * b) (v * v0)).
   rewrite <- H.
   replace (u * a + v * b) with ((u * a + v * b) * 1); [ idtac | ring ].
   rewrite <- H0.
@@ -447,7 +445,7 @@ Lemma rel_prime_cross_prod :
 Proof.
   intros a b c d; intros H H0 H1 H2 H3.
   elim (Z.divide_antisym b d).
-  - split; auto with zarith.
+  - intros H4; split; auto with zarith.
     rewrite H4 in H3.
     rewrite Z.mul_comm in H3.
     apply Z.mul_reg_l with d; auto.
@@ -473,9 +471,9 @@ Lemma Zis_gcd_rel_prime :
 Proof.
   intros a b g; intros H H0 H1.
   assert (H2 : g <> 0) by
-    (intro;
-    elim H1; intros;
-    elim H4; intros;
+    (intro H2;
+    elim H1; intros ? H4 ?;
+    elim H4; intros ? H6;
     rewrite H2 in H6; subst b;
     contradict H; rewrite Z.mul_0_r; discriminate).
   assert (H3 : g > 0) by
@@ -578,7 +576,7 @@ Lemma prime_divisors :
   forall p:Z,
     prime p -> forall a:Z, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p.
 Proof.
-  destruct 1; intros.
+  intros p; destruct 1 as [H H0]; intros a ?.
   assert
     (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p).
   { assert (Z.abs a <= Z.abs p) as H2.
@@ -602,12 +600,13 @@ Proof.
     }
   intuition idtac.
   (* -p < a < -1 *)
-  - absurd (rel_prime (- a) p).
+  - match goal with [hyp : a < -1 |- _] => rename hyp into H4 end.
+    absurd (rel_prime (- a) p).
     + intros [H1p H2p H3p].
       assert (- a | - a) by auto with zarith.
-      assert (- a | p) by auto with zarith.
+      assert (- a | p) as H5 by auto with zarith.
       apply H3p, Z.divide_1_r in H5; auto with zarith.
-      destruct H5.
+      destruct H5 as [H5|H5].
       * contradict H4; rewrite <- (Z.opp_involutive a), H5 .
         apply Z.lt_irrefl.
       * contradict H4; rewrite <- (Z.opp_involutive a), H5 .
@@ -616,16 +615,18 @@ Proof.
       * now apply Z.opp_le_mono; rewrite Z.opp_involutive; apply Z.lt_le_incl.
       * now apply Z.opp_lt_mono; rewrite Z.opp_involutive.
   (* a = 0 *)
-  - contradict H.
+  - match goal with [hyp : a = 0 |- _] => rename hyp into H2 end.
+    contradict H.
     replace p with 0; try discriminate.
     now apply sym_equal, Z.divide_0_l; rewrite <-H2.
   (* 1 < a < p *)
-  - absurd (rel_prime a p).
+  - match goal with [hyp : 1 < a |- _] => rename hyp into H3 end.
+    absurd (rel_prime a p).
     + intros [H1p H2p H3p].
       assert (a | a) by auto with zarith.
-      assert (a | p) by auto with zarith.
+      assert (a | p) as H5 by auto with zarith.
       apply H3p, Z.divide_1_r in H5; auto with zarith.
-      destruct H5.
+      destruct H5 as [H5|H5].
       * contradict H3; rewrite <- (Z.opp_involutive a), H5 .
         apply Z.lt_irrefl.
       * contradict H3; rewrite <- (Z.opp_involutive a), H5 .
@@ -639,7 +640,7 @@ Qed.
 Lemma prime_rel_prime :
   forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a.
 Proof.
-  intros; constructor; intros; auto with zarith.
+  intros p H a H0; constructor; auto with zarith; intros ? H1 H2.
   apply prime_divisors in H1; intuition; subst; auto with zarith.
   - absurd (p | a); auto with zarith.
   - absurd (p | a); intuition.
@@ -671,7 +672,7 @@ Qed.
 Lemma prime_mult :
   forall p:Z, prime p -> forall a b:Z, (p | a * b) -> (p | a) \/ (p | b).
 Proof.
-  intro p; simple induction 1; intros.
+  intro p; simple induction 1; intros ? ? a b ?.
   case (Zdivide_dec p a); intuition.
   right; apply Gauss with a; auto with zarith.
 Qed.
@@ -743,9 +744,9 @@ Proof.
     + now exists 1.
     + elim (H x); auto.
       split; trivial.
-      apply Z.le_lt_trans with n; try intuition.
+      apply Z.le_lt_trans with n; try tauto.
       apply Z.divide_pos_le; auto with zarith.
-      apply Z.lt_le_trans with (2 := H0); red; auto.
+      apply Z.lt_le_trans with (2 := proj1 Hn); red; auto.
   - (* prime' -> prime *)
     constructor; trivial. intros n Hn Hnp.
     case (Zis_gcd_unique n p n 1).
@@ -870,7 +871,7 @@ Hint Resolve Z.gcd_0_r Z.gcd_1_r : zarith.
 Theorem Zgcd_1_rel_prime : forall a b,
  Z.gcd a b = 1 <-> rel_prime a b.
 Proof.
-  unfold rel_prime; split; intro H.
+  unfold rel_prime; intros a b; split; intro H.
   rewrite <- H; apply Zgcd_is_gcd.
   case (Zis_gcd_unique a b (Z.gcd a b) 1); auto.
   apply Zgcd_is_gcd.
@@ -894,10 +895,10 @@ Definition prime_dec_aux:
 Proof.
   intros p m.
   case (Z_lt_dec 1 m); intros H1;
-   [ | left; intros; exfalso;
+   [ | left; intros n ?; exfalso;
        contradict H1; apply Z.lt_trans with n; intuition].
   pattern m; apply natlike_rec; auto with zarith.
-  - left; intros; exfalso.
+  - left; intros n ?; exfalso.
     absurd (1 < 0); try discriminate.
     apply Z.lt_trans with  n; intuition.
   - intros x Hx IH; destruct IH as [F|E].
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 7e33fe2b4c..949a01860f 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -354,7 +354,7 @@ Qed.
 
 Lemma Zle_0_nat : forall n:nat, 0 <= Z.of_nat n.
 Proof.
-  induction n; simpl; intros. apply Z.le_refl. easy.
+  intros n; induction n; simpl; intros. apply Z.le_refl. easy.
 Qed.
 
 Hint Immediate Z.eq_le_incl: zarith.
diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v
index 8609a6af98..d4f58c3b04 100644
--- a/theories/ZArith/Zpow_def.v
+++ b/theories/ZArith/Zpow_def.v
@@ -25,9 +25,9 @@ Notation Zpower_Ppow := Pos2Z.inj_pow (only parsing).
 
 Lemma Zpower_theory : power_theory 1 Z.mul (@eq Z) Z.of_N Z.pow.
 Proof.
- constructor. intros.
- destruct n;simpl;trivial.
+ constructor. intros z n.
+ destruct n as [|p];simpl;trivial.
  unfold Z.pow_pos.
  rewrite <- (Z.mul_1_r (pow_pos _ _ _)). generalize 1.
- induction p; simpl; intros; rewrite ?IHp, ?Z.mul_assoc; trivial.
+ induction p as [p IHp|p IHp|]; simpl; intros; rewrite ?IHp, ?Z.mul_assoc; trivial.
 Qed.