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

Reviewed-by: anton-trunov

12 files changed, 265 insertions, 265 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index 2361d59c26..0c097b6773 100644
--- a/theories/Numbers/Integer/Abstract/ZAdd.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -20,159 +20,157 @@ Include ZBaseProp Z.
 
 Hint Rewrite opp_0 : nz.
 
-Theorem add_pred_l : forall n m, P n + m == P (n + m).
+Theorem add_pred_l n m : P n + m == P (n + m).
 Proof.
-intros n m.
 rewrite <- (succ_pred n) at 2.
 now rewrite add_succ_l, pred_succ.
 Qed.
 
-Theorem add_pred_r : forall n m, n + P m == P (n + m).
+Theorem add_pred_r n m : n + P m == P (n + m).
 Proof.
-intros n m; rewrite 2 (add_comm n); apply add_pred_l.
+rewrite 2 (add_comm n); apply add_pred_l.
 Qed.
 
-Theorem add_opp_r : forall n m, n + (- m) == n - m.
+Theorem add_opp_r n m : n + (- m) == n - m.
 Proof.
 nzinduct m.
 now nzsimpl.
 intro m. rewrite opp_succ, sub_succ_r, add_pred_r. now rewrite pred_inj_wd.
 Qed.
 
-Theorem sub_0_l : forall n, 0 - n == - n.
+Theorem sub_0_l n : 0 - n == - n.
 Proof.
-intro n; rewrite <- add_opp_r; now rewrite add_0_l.
+rewrite <- add_opp_r; now rewrite add_0_l.
 Qed.
 
-Theorem sub_succ_l : forall n m, S n - m == S (n - m).
+Theorem sub_succ_l n m : S n - m == S (n - m).
 Proof.
-intros n m; rewrite <- 2 add_opp_r; now rewrite add_succ_l.
+rewrite <- 2 add_opp_r; now rewrite add_succ_l.
 Qed.
 
-Theorem sub_pred_l : forall n m, P n - m == P (n - m).
+Theorem sub_pred_l n m : P n - m == P (n - m).
 Proof.
-intros n m. rewrite <- (succ_pred n) at 2.
+rewrite <- (succ_pred n) at 2.
 rewrite sub_succ_l; now rewrite pred_succ.
 Qed.
 
-Theorem sub_pred_r : forall n m, n - (P m) == S (n - m).
+Theorem sub_pred_r n m : n - (P m) == S (n - m).
 Proof.
-intros n m. rewrite <- (succ_pred m) at 2.
+rewrite <- (succ_pred m) at 2.
 rewrite sub_succ_r; now rewrite succ_pred.
 Qed.
 
-Theorem opp_pred : forall n, - (P n) == S (- n).
+Theorem opp_pred n : - (P n) == S (- n).
 Proof.
-intro n. rewrite <- (succ_pred n) at 2.
+rewrite <- (succ_pred n) at 2.
 rewrite opp_succ. now rewrite succ_pred.
 Qed.
 
-Theorem sub_diag : forall n, n - n == 0.
+Theorem sub_diag n : n - n == 0.
 Proof.
 nzinduct n.
 now nzsimpl.
 intro n. rewrite sub_succ_r, sub_succ_l; now rewrite pred_succ.
 Qed.
 
-Theorem add_opp_diag_l : forall n, - n + n == 0.
+Theorem add_opp_diag_l n : - n + n == 0.
 Proof.
-intro n; now rewrite add_comm, add_opp_r, sub_diag.
+now rewrite add_comm, add_opp_r, sub_diag.
 Qed.
 
-Theorem add_opp_diag_r : forall n, n + (- n) == 0.
+Theorem add_opp_diag_r n : n + (- n) == 0.
 Proof.
-intro n; rewrite add_comm; apply add_opp_diag_l.
+rewrite add_comm; apply add_opp_diag_l.
 Qed.
 
-Theorem add_opp_l : forall n m, - m + n == n - m.
+Theorem add_opp_l n m : - m + n == n - m.
 Proof.
-intros n m; rewrite <- add_opp_r; now rewrite add_comm.
+rewrite <- add_opp_r; now rewrite add_comm.
 Qed.
 
-Theorem add_sub_assoc : forall n m p, n + (m - p) == (n + m) - p.
+Theorem add_sub_assoc n m p : n + (m - p) == (n + m) - p.
 Proof.
-intros n m p; rewrite <- 2 add_opp_r; now rewrite add_assoc.
+rewrite <- 2 add_opp_r; now rewrite add_assoc.
 Qed.
 
-Theorem opp_involutive : forall n, - (- n) == n.
+Theorem opp_involutive n : - (- n) == n.
 Proof.
 nzinduct n.
 now nzsimpl.
 intro n. rewrite opp_succ, opp_pred. now rewrite succ_inj_wd.
 Qed.
 
-Theorem opp_add_distr : forall n m, - (n + m) == - n + (- m).
+Theorem opp_add_distr n m : - (n + m) == - n + (- m).
 Proof.
-intros n m; nzinduct n.
+nzinduct n.
 now nzsimpl.
 intro n. rewrite add_succ_l; do 2 rewrite opp_succ; rewrite add_pred_l.
 now rewrite pred_inj_wd.
 Qed.
 
-Theorem opp_sub_distr : forall n m, - (n - m) == - n + m.
+Theorem opp_sub_distr n m : - (n - m) == - n + m.
 Proof.
-intros n m; rewrite <- add_opp_r, opp_add_distr.
+rewrite <- add_opp_r, opp_add_distr.
 now rewrite opp_involutive.
 Qed.
 
-Theorem opp_inj : forall n m, - n == - m -> n == m.
+Theorem opp_inj n m : - n == - m -> n == m.
 Proof.
-intros n m H. apply opp_wd in H. now rewrite 2 opp_involutive in H.
+intros H. apply opp_wd in H. now rewrite 2 opp_involutive in H.
 Qed.
 
-Theorem opp_inj_wd : forall n m, - n == - m <-> n == m.
+Theorem opp_inj_wd n m : - n == - m <-> n == m.
 Proof.
-intros n m; split; [apply opp_inj | intros; now f_equiv].
+split; [apply opp_inj | intros; now f_equiv].
 Qed.
 
-Theorem eq_opp_l : forall n m, - n == m <-> n == - m.
+Theorem eq_opp_l n m : - n == m <-> n == - m.
 Proof.
-intros n m. now rewrite <- (opp_inj_wd (- n) m), opp_involutive.
+now rewrite <- (opp_inj_wd (- n) m), opp_involutive.
 Qed.
 
-Theorem eq_opp_r : forall n m, n == - m <-> - n == m.
+Theorem eq_opp_r n m : n == - m <-> - n == m.
 Proof.
 symmetry; apply eq_opp_l.
 Qed.
 
-Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p.
+Theorem sub_add_distr n m p : n - (m + p) == (n - m) - p.
 Proof.
-intros n m p; rewrite <- add_opp_r, opp_add_distr, add_assoc.
+rewrite <- add_opp_r, opp_add_distr, add_assoc.
 now rewrite 2 add_opp_r.
 Qed.
 
-Theorem sub_sub_distr : forall n m p, n - (m - p) == (n - m) + p.
+Theorem sub_sub_distr n m p : n - (m - p) == (n - m) + p.
 Proof.
-intros n m p; rewrite <- add_opp_r, opp_sub_distr, add_assoc.
+rewrite <- add_opp_r, opp_sub_distr, add_assoc.
 now rewrite add_opp_r.
 Qed.
 
-Theorem sub_opp_l : forall n m, - n - m == - m - n.
+Theorem sub_opp_l n m : - n - m == - m - n.
 Proof.
-intros n m. rewrite <- 2 add_opp_r. now rewrite add_comm.
+rewrite <- 2 add_opp_r. now rewrite add_comm.
 Qed.
 
-Theorem sub_opp_r : forall n m, n - (- m) == n + m.
+Theorem sub_opp_r n m : n - (- m) == n + m.
 Proof.
-intros n m; rewrite <- add_opp_r; now rewrite opp_involutive.
+rewrite <- add_opp_r; now rewrite opp_involutive.
 Qed.
 
-Theorem add_sub_swap : forall n m p, n + m - p == n - p + m.
+Theorem add_sub_swap n m p : n + m - p == n - p + m.
 Proof.
-intros n m p. rewrite <- add_sub_assoc, <- (add_opp_r n p), <- add_assoc.
+rewrite <- add_sub_assoc, <- (add_opp_r n p), <- add_assoc.
 now rewrite add_opp_l.
 Qed.
 
-Theorem sub_cancel_l : forall n m p, n - m == n - p <-> m == p.
+Theorem sub_cancel_l n m p : n - m == n - p <-> m == p.
 Proof.
-intros n m p. rewrite <- (add_cancel_l (n - m) (n - p) (- n)).
+rewrite <- (add_cancel_l (n - m) (n - p) (- n)).
 rewrite 2 add_sub_assoc. rewrite add_opp_diag_l; rewrite 2 sub_0_l.
 apply opp_inj_wd.
 Qed.
 
-Theorem sub_cancel_r : forall n m p, n - p == m - p <-> n == m.
+Theorem sub_cancel_r n m p : n - p == m - p <-> n == m.
 Proof.
-intros n m p.
 stepl (n - p + p == m - p + p) by apply add_cancel_r.
 now do 2 rewrite <- sub_sub_distr, sub_diag, sub_0_r.
 Qed.
@@ -182,16 +180,15 @@ Qed.
     in the original equation ([add] or [sub]) and the indication
     whether the left or right term is moved. *)
 
-Theorem add_move_l : forall n m p, n + m == p <-> m == p - n.
+Theorem add_move_l n m p : n + m == p <-> m == p - n.
 Proof.
-intros n m p.
 stepl (n + m - n == p - n) by apply sub_cancel_r.
 now rewrite add_comm, <- add_sub_assoc, sub_diag, add_0_r.
 Qed.
 
-Theorem add_move_r : forall n m p, n + m == p <-> n == p - m.
+Theorem add_move_r n m p : n + m == p <-> n == p - m.
 Proof.
-intros n m p; rewrite add_comm; now apply add_move_l.
+rewrite add_comm; now apply add_move_l.
 Qed.
 
 (** The two theorems above do not allow rewriting subformulas of the
@@ -199,98 +196,98 @@ Qed.
     right-hand side of the equation. Hence the following two
     theorems. *)
 
-Theorem sub_move_l : forall n m p, n - m == p <-> - m == p - n.
+Theorem sub_move_l n m p : n - m == p <-> - m == p - n.
 Proof.
-intros n m p; rewrite <- (add_opp_r n m); apply add_move_l.
+rewrite <- (add_opp_r n m); apply add_move_l.
 Qed.
 
-Theorem sub_move_r : forall n m p, n - m == p <-> n == p + m.
+Theorem sub_move_r n m p : n - m == p <-> n == p + m.
 Proof.
-intros n m p; rewrite <- (add_opp_r n m). now rewrite add_move_r, sub_opp_r.
+rewrite <- (add_opp_r n m). now rewrite add_move_r, sub_opp_r.
 Qed.
 
-Theorem add_move_0_l : forall n m, n + m == 0 <-> m == - n.
+Theorem add_move_0_l n m : n + m == 0 <-> m == - n.
 Proof.
-intros n m; now rewrite add_move_l, sub_0_l.
+now rewrite add_move_l, sub_0_l.
 Qed.
 
-Theorem add_move_0_r : forall n m, n + m == 0 <-> n == - m.
+Theorem add_move_0_r n m : n + m == 0 <-> n == - m.
 Proof.
-intros n m; now rewrite add_move_r, sub_0_l.
+now rewrite add_move_r, sub_0_l.
 Qed.
 
-Theorem sub_move_0_l : forall n m, n - m == 0 <-> - m == - n.
+Theorem sub_move_0_l n m : n - m == 0 <-> - m == - n.
 Proof.
-intros n m. now rewrite sub_move_l, sub_0_l.
+now rewrite sub_move_l, sub_0_l.
 Qed.
 
-Theorem sub_move_0_r : forall n m, n - m == 0 <-> n == m.
+Theorem sub_move_0_r n m : n - m == 0 <-> n == m.
 Proof.
-intros n m. now rewrite sub_move_r, add_0_l.
+now rewrite sub_move_r, add_0_l.
 Qed.
 
 (** The following section is devoted to cancellation of like
     terms. The name includes the first operator and the position of
     the term being canceled. *)
 
-Theorem add_simpl_l : forall n m, n + m - n == m.
+Theorem add_simpl_l n m : n + m - n == m.
 Proof.
-intros; now rewrite add_sub_swap, sub_diag, add_0_l.
+now rewrite add_sub_swap, sub_diag, add_0_l.
 Qed.
 
-Theorem add_simpl_r : forall n m, n + m - m == n.
+Theorem add_simpl_r n m : n + m - m == n.
 Proof.
-intros; now rewrite <- add_sub_assoc, sub_diag, add_0_r.
+now rewrite <- add_sub_assoc, sub_diag, add_0_r.
 Qed.
 
-Theorem sub_simpl_l : forall n m, - n - m + n == - m.
+Theorem sub_simpl_l n m : - n - m + n == - m.
 Proof.
-intros; now rewrite <- add_sub_swap, add_opp_diag_l, sub_0_l.
+now rewrite <- add_sub_swap, add_opp_diag_l, sub_0_l.
 Qed.
 
-Theorem sub_simpl_r : forall n m, n - m + m == n.
+Theorem sub_simpl_r n m : n - m + m == n.
 Proof.
-intros; now rewrite <- sub_sub_distr, sub_diag, sub_0_r.
+now rewrite <- sub_sub_distr, sub_diag, sub_0_r.
 Qed.
 
-Theorem sub_add : forall n m, m - n + n == m.
+Theorem sub_add n m : m - n + n == m.
 Proof.
- intros. now rewrite <- add_sub_swap, add_simpl_r.
+now rewrite <- add_sub_swap, add_simpl_r.
 Qed.
 
 (** Now we have two sums or differences; the name includes the two
     operators and the position of the terms being canceled *)
 
-Theorem add_add_simpl_l_l : forall n m p, (n + m) - (n + p) == m - p.
+Theorem add_add_simpl_l_l n m p : (n + m) - (n + p) == m - p.
 Proof.
-intros n m p. now rewrite (add_comm n m), <- add_sub_assoc,
+now rewrite (add_comm n m), <- add_sub_assoc,
 sub_add_distr, sub_diag, sub_0_l, add_opp_r.
 Qed.
 
-Theorem add_add_simpl_l_r : forall n m p, (n + m) - (p + n) == m - p.
+Theorem add_add_simpl_l_r n m p : (n + m) - (p + n) == m - p.
 Proof.
-intros n m p. rewrite (add_comm p n); apply add_add_simpl_l_l.
+rewrite (add_comm p n); apply add_add_simpl_l_l.
 Qed.
 
-Theorem add_add_simpl_r_l : forall n m p, (n + m) - (m + p) == n - p.
+Theorem add_add_simpl_r_l n m p : (n + m) - (m + p) == n - p.
 Proof.
-intros n m p. rewrite (add_comm n m); apply add_add_simpl_l_l.
+rewrite (add_comm n m); apply add_add_simpl_l_l.
 Qed.
 
-Theorem add_add_simpl_r_r : forall n m p, (n + m) - (p + m) == n - p.
+Theorem add_add_simpl_r_r n m p : (n + m) - (p + m) == n - p.
 Proof.
-intros n m p. rewrite (add_comm p m); apply add_add_simpl_r_l.
+rewrite (add_comm p m); apply add_add_simpl_r_l.
 Qed.
 
-Theorem sub_add_simpl_r_l : forall n m p, (n - m) + (m + p) == n + p.
+Theorem sub_add_simpl_r_l n m p : (n - m) + (m + p) == n + p.
 Proof.
-intros n m p. now rewrite <- sub_sub_distr, sub_add_distr, sub_diag,
+now rewrite <- sub_sub_distr, sub_add_distr, sub_diag,
 sub_0_l, sub_opp_r.
 Qed.
 
-Theorem sub_add_simpl_r_r : forall n m p, (n - m) + (p + m) == n + p.
+Theorem sub_add_simpl_r_r n m p : (n - m) + (p + m) == n + p.
 Proof.
-intros n m p. rewrite (add_comm p m); apply sub_add_simpl_r_l.
+rewrite (add_comm p m); apply sub_add_simpl_r_l.
 Qed.
 
 (** Of course, there are many other variants *)
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index 40a37be5f9..5a293c6483 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -241,25 +241,25 @@ Qed.
 
 Theorem sub_neg_cases : forall n m, n - m < 0 -> n < 0 \/ 0 < m.
 Proof.
-intros.
+intros n m ?.
 rewrite <- (opp_neg_pos m). apply add_neg_cases. now rewrite add_opp_r.
 Qed.
 
 Theorem sub_pos_cases : forall n m, 0 < n - m -> 0 < n \/ m < 0.
 Proof.
-intros.
+intros n m ?.
 rewrite <- (opp_pos_neg m). apply add_pos_cases. now rewrite add_opp_r.
 Qed.
 
 Theorem sub_nonpos_cases : forall n m, n - m <= 0 -> n <= 0 \/ 0 <= m.
 Proof.
-intros.
+intros n m ?.
 rewrite <- (opp_nonpos_nonneg m). apply add_nonpos_cases. now rewrite add_opp_r.
 Qed.
 
 Theorem sub_nonneg_cases : forall n m, 0 <= n - m -> 0 <= n \/ m <= 0.
 Proof.
-intros.
+intros n m ?.
 rewrite <- (opp_nonneg_nonpos m). apply add_nonneg_cases. now rewrite add_opp_r.
 Qed.
 
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index 0f40d3d7b6..4d2361689d 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -244,7 +244,7 @@ Qed.
 
 Lemma bit0_odd : forall a, a.[0] = odd a.
 Proof.
- intros. symmetry.
+ intros a. symmetry.
  destruct (exists_div2 a) as (a' & b & EQ).
  rewrite EQ, testbit_0_r, add_comm, odd_add_mul_2.
  destruct b; simpl; apply odd_1 || apply odd_0.
@@ -428,14 +428,14 @@ Qed.
 
 Lemma mul_pow2_bits : forall a n m, 0<=n -> (a*2^n).[m] = a.[m-n].
 Proof.
- intros.
+ intros a n m ?.
  rewrite <- (add_simpl_r m n) at 1. rewrite add_sub_swap, add_comm.
  now apply mul_pow2_bits_add.
 Qed.
 
 Lemma mul_pow2_bits_low : forall a n m, m<n -> (a*2^n).[m] = false.
 Proof.
- intros.
+ intros a n m ?.
  destruct (le_gt_cases 0 n).
  rewrite mul_pow2_bits by trivial.
  apply testbit_neg_r. now apply lt_sub_0.
@@ -561,7 +561,10 @@ Proof.
  split. apply bits_inj'. intros EQ n Hn; now rewrite EQ.
 Qed.
 
-Ltac bitwise := apply bits_inj'; intros ?m ?Hm; autorewrite with bitwise.
+Tactic Notation "bitwise" "as" simple_intropattern(m) simple_intropattern(Hm)
+  := apply bits_inj'; intros m Hm; autorewrite with bitwise.
+
+Ltac bitwise := bitwise as ?m ?Hm.
 
 Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise.
 
@@ -619,7 +622,7 @@ Qed.
 
 Lemma shiftl_spec : forall a n m, 0<=m -> (a << n).[m] = a.[m-n].
 Proof.
- intros.
+ intros a n m ?.
  destruct (le_gt_cases n m).
  now apply shiftl_spec_high.
  rewrite shiftl_spec_low, testbit_neg_r; trivial. now apply lt_sub_0.
@@ -693,7 +696,7 @@ Qed.
 Lemma shiftl_shiftl : forall a n m, 0<=n ->
  (a << n) << m == a << (n+m).
 Proof.
- intros a n p Hn. bitwise.
+ intros a n p Hn. bitwise as m Hm.
  rewrite 2 (shiftl_spec _ _ m) by trivial.
  rewrite add_comm, sub_add_distr.
  destruct (le_gt_cases 0 (m-p)) as [H|H].
@@ -745,8 +748,8 @@ Qed.
 
 Lemma shiftl_0_l : forall n, 0 << n == 0.
 Proof.
- intros.
- destruct (le_ge_cases 0 n).
+ intros n.
+ destruct (le_ge_cases 0 n) as [H|H].
  rewrite shiftl_mul_pow2 by trivial. now nzsimpl.
  rewrite shiftl_div_pow2 by trivial.
  rewrite <- opp_nonneg_nonpos in H. nzsimpl; order_nz.
@@ -901,7 +904,7 @@ Qed.
 
 Lemma lor_eq_0_l : forall a b, lor a b == 0 -> a == 0.
 Proof.
- intros a b H. bitwise.
+ intros a b H. bitwise as m ?.
  apply (orb_false_iff a.[m] b.[m]).
  now rewrite <- lor_spec, H, bits_0.
 Qed.
@@ -909,7 +912,7 @@ Qed.
 Lemma lor_eq_0_iff : forall a b, lor a b == 0 <-> a == 0 /\ b == 0.
 Proof.
  intros a b. split.
- split. now apply lor_eq_0_l in H.
+ intro H; split. now apply lor_eq_0_l in H.
  rewrite lor_comm in H. now apply lor_eq_0_l in H.
  intros (EQ,EQ'). now rewrite EQ, lor_0_l.
 Qed.
@@ -1022,13 +1025,13 @@ Proof. unfold clearbit. solve_proper. Qed.
 
 Lemma pow2_bits_true : forall n, 0<=n -> (2^n).[n] = true.
 Proof.
- intros. rewrite <- (mul_1_l (2^n)).
+ intros n ?. rewrite <- (mul_1_l (2^n)).
  now rewrite mul_pow2_bits, sub_diag, bit0_odd, odd_1.
 Qed.
 
 Lemma pow2_bits_false : forall n m, n~=m -> (2^n).[m] = false.
 Proof.
- intros.
+ intros n m ?.
  destruct (le_gt_cases 0 n); [|now rewrite pow_neg_r, bits_0].
  destruct (le_gt_cases n m).
  rewrite <- (mul_1_l (2^n)), mul_pow2_bits; trivial.
@@ -1073,7 +1076,7 @@ Qed.
 Lemma clearbit_eqb : forall a n m,
  (clearbit a n).[m] = a.[m] && negb (eqb n m).
 Proof.
- intros.
+ intros a n m.
  destruct (le_gt_cases 0 m); [| now rewrite 2 testbit_neg_r].
  rewrite clearbit_spec', ldiff_spec. f_equal. f_equal.
  destruct (le_gt_cases 0 n) as [Hn|Hn].
@@ -1090,7 +1093,7 @@ Qed.
 
 Lemma clearbit_eq : forall a n, (clearbit a n).[n] = false.
 Proof.
- intros. rewrite clearbit_eqb, (proj2 (eqb_eq _ _) (eq_refl n)).
+ intros a n. rewrite clearbit_eqb, (proj2 (eqb_eq _ _) (eq_refl n)).
  apply andb_false_r.
 Qed.
 
@@ -1161,7 +1164,7 @@ Proof. unfold lnot. solve_proper. Qed.
 
 Lemma lnot_spec : forall a n, 0<=n -> (lnot a).[n] = negb a.[n].
 Proof.
- intros. unfold lnot. rewrite <- (opp_involutive a) at 2.
+ intros a n ?. unfold lnot. rewrite <- (opp_involutive a) at 2.
  rewrite bits_opp, negb_involutive; trivial.
 Qed.
 
@@ -1214,7 +1217,7 @@ Qed.
 
 Lemma lor_lnot_diag : forall a, lor a (lnot a) == -1.
 Proof.
- intros a. bitwise. rewrite lnot_spec, bits_m1; trivial.
+ intros a. bitwise as m ?. rewrite lnot_spec, bits_m1; trivial.
  now destruct a.[m].
 Qed.
 
@@ -1267,7 +1270,7 @@ Qed.
 
 Lemma lxor_m1_r : forall a, lxor a (-1) == lnot a.
 Proof.
- intros. now rewrite <- (lxor_0_r (lnot a)), <- lnot_m1, lxor_lnot_lnot.
+ intros a. now rewrite <- (lxor_0_r (lnot a)), <- lnot_m1, lxor_lnot_lnot.
 Qed.
 
 Lemma lxor_m1_l : forall a, lxor (-1) a == lnot a.
@@ -1278,7 +1281,7 @@ Qed.
 Lemma lxor_lor : forall a b, land a b == 0 ->
  lxor a b == lor a b.
 Proof.
- intros a b H. bitwise.
+ intros a b H. bitwise as m ?.
  assert (a.[m] && b.[m] = false)
    by now rewrite <- land_spec, H, bits_0.
  now destruct a.[m], b.[m].
@@ -1299,7 +1302,7 @@ Proof. unfold ones. solve_proper. Qed.
 
 Lemma ones_equiv : forall n, ones n == P (2^n).
 Proof.
- intros. unfold ones.
+ intros n. unfold ones.
  destruct (le_gt_cases 0 n).
  now rewrite shiftl_mul_pow2, mul_1_l.
  f_equiv. rewrite pow_neg_r; trivial.
@@ -1367,7 +1370,7 @@ Qed.
 Lemma lor_ones_low : forall a n, 0<=a -> log2 a < n ->
  lor a (ones n) == ones n.
 Proof.
- intros a n Ha H. bitwise. destruct (le_gt_cases n m).
+ intros a n Ha H. bitwise as m ?. destruct (le_gt_cases n m).
  rewrite ones_spec_high, bits_above_log2; try split; trivial.
  now apply lt_le_trans with n.
  apply le_trans with (log2 a); order_pos.
@@ -1376,7 +1379,7 @@ Qed.
 
 Lemma land_ones : forall a n, 0<=n -> land a (ones n) == a mod 2^n.
 Proof.
- intros a n Hn. bitwise. destruct (le_gt_cases n m).
+ intros a n Hn. bitwise as m ?. destruct (le_gt_cases n m).
  rewrite ones_spec_high, mod_pow2_bits_high, andb_false_r;
   try split; trivial.
  rewrite ones_spec_low, mod_pow2_bits_low, andb_true_r;
@@ -1396,7 +1399,7 @@ Qed.
 Lemma ldiff_ones_r : forall a n, 0<=n ->
  ldiff a (ones n) == (a >> n) << n.
 Proof.
- intros a n Hn. bitwise. destruct (le_gt_cases n m).
+ intros a n Hn. bitwise as m ?. destruct (le_gt_cases n m).
  rewrite ones_spec_high, shiftl_spec_high, shiftr_spec; trivial.
  rewrite sub_add; trivial. apply andb_true_r.
  now apply le_0_sub.
@@ -1408,7 +1411,7 @@ Qed.
 Lemma ldiff_ones_r_low : forall a n, 0<=a -> log2 a < n ->
  ldiff a (ones n) == 0.
 Proof.
- intros a n Ha H. bitwise. destruct (le_gt_cases n m).
+ intros a n Ha H. bitwise as m ?. destruct (le_gt_cases n m).
  rewrite ones_spec_high, bits_above_log2; trivial.
  now apply lt_le_trans with n.
  split; trivial. now apply le_trans with (log2 a); order_pos.
@@ -1418,7 +1421,7 @@ Qed.
 Lemma ldiff_ones_l_low : forall a n, 0<=a -> log2 a < n ->
  ldiff (ones n) a == lxor a (ones n).
 Proof.
- intros a n Ha H. bitwise. destruct (le_gt_cases n m).
+ intros a n Ha H. bitwise as m ?. destruct (le_gt_cases n m).
  rewrite ones_spec_high, bits_above_log2; trivial.
  now apply lt_le_trans with n.
  split; trivial. now apply le_trans with (log2 a); order_pos.
@@ -1585,7 +1588,7 @@ Qed.
 Lemma log2_shiftr : forall a n, 0<a -> log2 (a >> n) == max 0 (log2 a - n).
 Proof.
  intros a n Ha.
- destruct (le_gt_cases 0 (log2 a - n));
+ destruct (le_gt_cases 0 (log2 a - n)) as [H|H];
    [rewrite max_r | rewrite max_l]; try order.
  apply log2_bits_unique.
  now rewrite shiftr_spec, sub_add, bit_log2.
@@ -1698,7 +1701,7 @@ Qed.
 Lemma add_carry_div2 : forall a b (c0:bool),
  (a + b + c0)/2 == a/2 + b/2 + nextcarry a.[0] b.[0] c0.
 Proof.
- intros.
+ intros a b c0.
  rewrite <- add3_bits_div2.
  rewrite (add_comm ((a/2)+_)).
  rewrite <- div_add by order'.
@@ -1767,7 +1770,7 @@ Proof.
  apply div_lt_upper_bound. order'. now rewrite <- pow_succ_r.
  exists (c0 + 2*c). repeat split.
  (* step, add *)
- bitwise.
+ bitwise as m Hm.
  le_elim Hm.
  rewrite <- (succ_pred m), lt_succ_r in Hm.
  rewrite <- (succ_pred m), <- !div2_bits, <- 2 lxor_spec by trivial.
@@ -1777,7 +1780,7 @@ Proof.
  now rewrite add_b2z_double_bit0, add3_bit0, b2z_bit0.
  (* step, carry *)
  rewrite add_b2z_double_div2.
- bitwise.
+ bitwise as m Hm.
  le_elim Hm.
  rewrite <- (succ_pred m), lt_succ_r in Hm.
  rewrite <- (succ_pred m), <- !div2_bits, IH2 by trivial.
@@ -1905,7 +1908,7 @@ Proof.
  rewrite sub_add.
  symmetry.
  rewrite add_nocarry_lxor; trivial.
- bitwise.
+ bitwise as m ?.
  apply bits_inj_iff in H. specialize (H m).
  rewrite ldiff_spec, bits_0 in H.
  now destruct a.[m], b.[m].
@@ -1938,7 +1941,7 @@ Lemma add_nocarry_mod_lt_pow2 : forall a b n, 0<=n -> land a b == 0 ->
 Proof.
  intros a b n Hn H.
  apply add_nocarry_lt_pow2.
- bitwise.
+ bitwise as m ?.
  destruct (le_gt_cases n m).
  rewrite mod_pow2_bits_high; now split.
  now rewrite !mod_pow2_bits_low, <- land_spec, H, bits_0.
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index 44cba37eb2..d28d010ae8 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -51,7 +51,7 @@ Qed.
 Lemma mod_bound_abs :
  forall a b, b~=0 -> abs (a mod b) < abs b.
 Proof.
-intros.
+intros a b **.
 destruct (abs_spec b) as [(LE,EQ)|(LE,EQ)]; rewrite EQ.
 destruct (mod_pos_bound a b). order. now rewrite abs_eq.
 destruct (mod_neg_bound a b). order. rewrite abs_neq; trivial.
@@ -87,11 +87,11 @@ Qed.
 
 Theorem div_unique_pos:
  forall a b q r, 0<=r<b -> a == b*q + r -> q == a/b.
-Proof. intros; apply div_unique with r; auto. Qed.
+Proof. intros a b q r **; apply div_unique with r; auto. Qed.
 
 Theorem div_unique_neg:
  forall a b q r, b<r<=0 -> a == b*q + r -> q == a/b.
-Proof. intros; apply div_unique with r; auto. Qed.
+Proof. intros a b q r **; apply div_unique with r; auto. Qed.
 
 Theorem mod_unique:
  forall a b q r, (0<=r<b \/ b<r<=0) -> a == b*q + r -> r == a mod b.
@@ -106,11 +106,11 @@ Qed.
 
 Theorem mod_unique_pos:
  forall a b q r, 0<=r<b -> a == b*q + r -> r == a mod b.
-Proof. intros; apply mod_unique with q; auto. Qed.
+Proof. intros a b q r **; apply mod_unique with q; auto. Qed.
 
 Theorem mod_unique_neg:
  forall a b q r, b<r<=0 -> a == b*q + r -> r == a mod b.
-Proof. intros; apply mod_unique with q; auto. Qed.
+Proof. intros a b q r **; apply mod_unique with q; auto. Qed.
 
 (** Sign rules *)
 
@@ -121,7 +121,7 @@ Ltac pos_or_neg a :=
 
 Fact mod_bound_or : forall a b, b~=0 -> 0<=a mod b<b \/ b<a mod b<=0.
 Proof.
-intros.
+intros a b **.
 destruct (lt_ge_cases 0 b); [left|right].
  apply mod_pos_bound; trivial. apply mod_neg_bound; order.
 Qed.
@@ -129,7 +129,7 @@ Qed.
 Fact opp_mod_bound_or : forall a b, b~=0 ->
  0 <= -(a mod b) < -b \/ -b < -(a mod b) <= 0.
 Proof.
-intros.
+intros a b **.
 destruct (lt_ge_cases 0 b); [right|left].
 rewrite <- opp_lt_mono, opp_nonpos_nonneg.
  destruct (mod_pos_bound a b); intuition; order.
@@ -139,14 +139,14 @@ Qed.
 
 Lemma div_opp_opp : forall a b, b~=0 -> -a/-b == a/b.
 Proof.
-intros. symmetry. apply div_unique with (- (a mod b)).
+intros a b **. symmetry. apply div_unique with (- (a mod b)).
 now apply opp_mod_bound_or.
 rewrite mul_opp_l, <- opp_add_distr, <- div_mod; order.
 Qed.
 
 Lemma mod_opp_opp : forall a b, b~=0 -> (-a) mod (-b) == - (a mod b).
 Proof.
-intros. symmetry. apply mod_unique with (a/b).
+intros a b **. symmetry. apply mod_unique with (a/b).
 now apply opp_mod_bound_or.
 rewrite mul_opp_l, <- opp_add_distr, <- div_mod; order.
 Qed.
@@ -200,28 +200,28 @@ Qed.
 Lemma div_opp_r_z :
  forall a b, b~=0 -> a mod b == 0 -> a/(-b) == -(a/b).
 Proof.
-intros. rewrite <- (opp_involutive a) at 1.
+intros a b **. rewrite <- (opp_involutive a) at 1.
 rewrite div_opp_opp; auto using div_opp_l_z.
 Qed.
 
 Lemma div_opp_r_nz :
  forall a b, b~=0 -> a mod b ~= 0 -> a/(-b) == -(a/b)-1.
 Proof.
-intros. rewrite <- (opp_involutive a) at 1.
+intros a b **. rewrite <- (opp_involutive a) at 1.
 rewrite div_opp_opp; auto using div_opp_l_nz.
 Qed.
 
 Lemma mod_opp_r_z :
  forall a b, b~=0 -> a mod b == 0 -> a mod (-b) == 0.
 Proof.
-intros. rewrite <- (opp_involutive a) at 1.
+intros a b **. rewrite <- (opp_involutive a) at 1.
 now rewrite mod_opp_opp, mod_opp_l_z, opp_0.
 Qed.
 
 Lemma mod_opp_r_nz :
  forall a b, b~=0 -> a mod b ~= 0 -> a mod (-b) == (a mod b) - b.
 Proof.
-intros. rewrite <- (opp_involutive a) at 1.
+intros a b **. rewrite <- (opp_involutive a) at 1.
 rewrite mod_opp_opp, mod_opp_l_nz by trivial.
 now rewrite opp_sub_distr, add_comm, add_opp_r.
 Qed.
@@ -247,7 +247,7 @@ Qed.
 
 Lemma mod_sign_mul : forall a b, b~=0 -> 0 <= (a mod b) * b.
 Proof.
-intros. destruct (lt_ge_cases 0 b).
+intros a b **. destruct (lt_ge_cases 0 b).
 apply mul_nonneg_nonneg; destruct (mod_pos_bound a b); order.
 apply mul_nonpos_nonpos; destruct (mod_neg_bound a b); order.
 Qed.
@@ -256,7 +256,7 @@ Qed.
 
 Lemma div_same : forall a, a~=0 -> a/a == 1.
 Proof.
-intros. pos_or_neg a. apply div_same; order.
+intros a ?. pos_or_neg a. apply div_same; order.
 rewrite <- div_opp_opp by trivial. now apply div_same.
 Qed.
 
@@ -279,7 +279,7 @@ Proof. exact mod_small. Qed.
 
 Lemma div_0_l: forall a, a~=0 -> 0/a == 0.
 Proof.
-intros. pos_or_neg a. apply div_0_l; order.
+intros a ?. pos_or_neg a. apply div_0_l; order.
 rewrite <- div_opp_opp, opp_0 by trivial. now apply div_0_l.
 Qed.
 
@@ -308,7 +308,7 @@ Proof. exact mod_1_l. Qed.
 
 Lemma div_mul : forall a b, b~=0 -> (a*b)/b == a.
 Proof.
-intros. symmetry. apply div_unique with 0.
+intros a b ?. symmetry. apply div_unique with 0.
 destruct (lt_ge_cases 0 b); [left|right]; split; order.
 nzsimpl; apply mul_comm.
 Qed.
@@ -350,7 +350,7 @@ Qed.
 
 Lemma mod_small_iff : forall a b, b~=0 -> (a mod b == a <-> 0<=a<b \/ b<a<=0).
 Proof.
-intros.
+intros a b **.
 rewrite <- div_small_iff, mod_eq by trivial.
 rewrite sub_move_r, <- (add_0_r a) at 1. rewrite add_cancel_l.
 rewrite eq_sym_iff, eq_mul_0. tauto.
@@ -393,7 +393,7 @@ Qed.
 
 Lemma mul_div_le : forall a b, 0<b -> b*(a/b) <= a.
 Proof.
-intros.
+intros a b **.
 rewrite (div_mod a b) at 2; try order.
 rewrite <- (add_0_r (b*(a/b))) at 1.
 rewrite <- add_le_mono_l.
@@ -412,7 +412,7 @@ Qed.
 
 Lemma mul_succ_div_gt: forall a b, 0<b -> a < b*(S (a/b)).
 Proof.
-intros.
+intros a b ?.
 nzsimpl.
 rewrite (div_mod a b) at 1; try order.
 rewrite <- add_lt_mono_l.
@@ -432,7 +432,7 @@ Qed.
 
 Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0).
 Proof.
-intros.
+intros a b **.
 rewrite (div_mod a b) at 1; try order.
 rewrite <- (add_0_r (b*(a/b))) at 2.
 apply add_cancel_l.
@@ -443,7 +443,7 @@ Qed.
 Theorem div_lt_upper_bound:
   forall a b q, 0<b -> a < b*q -> a/b < q.
 Proof.
-intros.
+intros a b q **.
 rewrite (mul_lt_mono_pos_l b) by trivial.
 apply le_lt_trans with a; trivial.
 now apply mul_div_le.
@@ -452,7 +452,7 @@ Qed.
 Theorem div_le_upper_bound:
   forall a b q, 0<b -> a <= b*q -> a/b <= q.
 Proof.
-intros.
+intros a b q **.
 rewrite <- (div_mul q b) by order.
 apply div_le_mono; trivial. now rewrite mul_comm.
 Qed.
@@ -460,7 +460,7 @@ Qed.
 Theorem div_le_lower_bound:
   forall a b q, 0<b -> b*q <= a -> q <= a/b.
 Proof.
-intros.
+intros a b q **.
 rewrite <- (div_mul q b) by order.
 apply div_le_mono; trivial. now rewrite mul_comm.
 Qed.
@@ -475,7 +475,7 @@ Proof. exact div_le_compat_l. Qed.
 Lemma mod_add : forall a b c, c~=0 ->
  (a + b * c) mod c == a mod c.
 Proof.
-intros.
+intros a b c **.
 symmetry.
 apply mod_unique with (a/c+b); trivial.
 now apply mod_bound_or.
@@ -486,7 +486,7 @@ Qed.
 Lemma div_add : forall a b c, c~=0 ->
  (a + b * c) / c == a / c + b.
 Proof.
-intros.
+intros a b c **.
 apply (mul_cancel_l _ _ c); try order.
 apply (add_cancel_r _ _ ((a+b*c) mod c)).
 rewrite <- div_mod, mod_add by order.
@@ -506,7 +506,7 @@ Qed.
 Lemma div_mul_cancel_r : forall a b c, b~=0 -> c~=0 ->
  (a*c)/(b*c) == a/b.
 Proof.
-intros.
+intros a b c **.
 symmetry.
 apply div_unique with ((a mod b)*c).
 (* ineqs *)
@@ -525,13 +525,13 @@ Qed.
 Lemma div_mul_cancel_l : forall a b c, b~=0 -> c~=0 ->
  (c*a)/(c*b) == a/b.
 Proof.
-intros. rewrite !(mul_comm c); now apply div_mul_cancel_r.
+intros a b c **. rewrite !(mul_comm c); now apply div_mul_cancel_r.
 Qed.
 
 Lemma mul_mod_distr_l: forall a b c, b~=0 -> c~=0 ->
   (c*a) mod (c*b) == c * (a mod b).
 Proof.
-intros.
+intros a b c **.
 rewrite <- (add_cancel_l _ _ ((c*b)* ((c*a)/(c*b)))).
 rewrite <- div_mod.
 rewrite div_mul_cancel_l by trivial.
@@ -543,7 +543,7 @@ Qed.
 Lemma mul_mod_distr_r: forall a b c, b~=0 -> c~=0 ->
   (a*c) mod (b*c) == (a mod b) * c.
 Proof.
- intros. rewrite !(mul_comm _ c); now rewrite mul_mod_distr_l.
+ intros a b c **. rewrite !(mul_comm _ c); now rewrite mul_mod_distr_l.
 Qed.
 
 
@@ -570,7 +570,7 @@ Qed.
 Lemma mul_mod_idemp_r : forall a b n, n~=0 ->
  (a*(b mod n)) mod n == (a*b) mod n.
 Proof.
- intros. rewrite !(mul_comm a). now apply mul_mod_idemp_l.
+ intros a b n **. rewrite !(mul_comm a). now apply mul_mod_idemp_l.
 Qed.
 
 Theorem mul_mod: forall a b n, n~=0 ->
@@ -591,7 +591,7 @@ Qed.
 Lemma add_mod_idemp_r : forall a b n, n~=0 ->
  (a+(b mod n)) mod n == (a+b) mod n.
 Proof.
- intros. rewrite !(add_comm a). now apply add_mod_idemp_l.
+ intros a b n **. rewrite !(add_comm a). now apply add_mod_idemp_l.
 Qed.
 
 Theorem add_mod: forall a b n, n~=0 ->
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 4915d69c5b..7d374bd4be 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -69,7 +69,7 @@ Proof. intros. now rewrite rem_opp_r, rem_opp_l. Qed.
 
 Lemma quot_opp_l : forall a b, b ~= 0 -> (-a)÷b == -(a÷b).
 Proof.
-intros.
+intros a b ?.
 rewrite <- (mul_cancel_l _ _ b) by trivial.
 rewrite <- (add_cancel_r _ _ ((-a) rem b)).
 now rewrite <- quot_rem, rem_opp_l, mul_opp_r, <- opp_add_distr, <- quot_rem.
@@ -77,7 +77,7 @@ Qed.
 
 Lemma quot_opp_r : forall a b, b ~= 0 -> a÷(-b) == -(a÷b).
 Proof.
-intros.
+intros a b ?.
 assert (-b ~= 0) by (now rewrite eq_opp_l, opp_0).
 rewrite <- (mul_cancel_l _ _ (-b)) by trivial.
 rewrite <- (add_cancel_r _ _ (a rem (-b))).
@@ -105,17 +105,17 @@ Qed.
 
 Theorem quot_unique:
  forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> q == a÷b.
-Proof. intros; now apply NZQuot.div_unique with r. Qed.
+Proof. intros a b q r **; now apply NZQuot.div_unique with r. Qed.
 
 Theorem rem_unique:
  forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> r == a rem b.
-Proof. intros; now apply NZQuot.mod_unique with q. Qed.
+Proof. intros a b q r **; now apply NZQuot.mod_unique with q. Qed.
 
 (** A division by itself returns 1 *)
 
 Lemma quot_same : forall a, a~=0 -> a÷a == 1.
 Proof.
-intros. pos_or_neg a. apply NZQuot.div_same; order.
+intros a ?. pos_or_neg a. apply NZQuot.div_same; order.
 rewrite <- quot_opp_opp by trivial. now apply NZQuot.div_same.
 Qed.
 
@@ -138,7 +138,7 @@ Proof. exact NZQuot.mod_small. Qed.
 
 Lemma quot_0_l: forall a, a~=0 -> 0÷a == 0.
 Proof.
-intros. pos_or_neg a. apply NZQuot.div_0_l; order.
+intros a ?. pos_or_neg a. apply NZQuot.div_0_l; order.
 rewrite <- quot_opp_opp, opp_0 by trivial. now apply NZQuot.div_0_l.
 Qed.
 
@@ -149,7 +149,7 @@ Qed.
 
 Lemma quot_1_r: forall a, a÷1 == a.
 Proof.
-intros. pos_or_neg a. now apply NZQuot.div_1_r.
+intros a. pos_or_neg a. now apply NZQuot.div_1_r.
 apply opp_inj. rewrite <- quot_opp_l. apply NZQuot.div_1_r; order.
 intro EQ; symmetry in EQ; revert EQ; apply lt_neq, lt_0_1.
 Qed.
@@ -168,7 +168,7 @@ Proof. exact NZQuot.mod_1_l. Qed.
 
 Lemma quot_mul : forall a b, b~=0 -> (a*b)÷b == a.
 Proof.
-intros. pos_or_neg a; pos_or_neg b. apply NZQuot.div_mul; order.
+intros a b ?. pos_or_neg a; pos_or_neg b. apply NZQuot.div_mul; order.
 rewrite <- quot_opp_opp, <- mul_opp_r by order. apply NZQuot.div_mul; order.
 rewrite <- opp_inj_wd, <- quot_opp_l, <- mul_opp_l by order.
 apply NZQuot.div_mul; order.
@@ -190,7 +190,7 @@ Qed.
 
 Lemma rem_nonneg : forall a b, b~=0 -> 0 <= a -> 0 <= a rem b.
 Proof.
- intros. pos_or_neg b. destruct (rem_bound_pos a b); order.
+ intros a b **. pos_or_neg b. destruct (rem_bound_pos a b); order.
  rewrite <- rem_opp_r; trivial.
  destruct (rem_bound_pos a (-b)); trivial.
 Qed.
@@ -309,7 +309,7 @@ Proof. exact NZQuot.div_str_pos. Qed.
 
 Lemma quot_small_iff : forall a b, b~=0 -> (a÷b==0 <-> abs a < abs b).
 Proof.
-intros. pos_or_neg a; pos_or_neg b.
+intros a b ?. pos_or_neg a; pos_or_neg b.
 rewrite NZQuot.div_small_iff; try order. rewrite 2 abs_eq; intuition; order.
 rewrite <- opp_inj_wd, opp_0, <- quot_opp_r, NZQuot.div_small_iff by order.
  rewrite (abs_eq a), (abs_neq' b); intuition; order.
@@ -321,7 +321,7 @@ Qed.
 
 Lemma rem_small_iff : forall a b, b~=0 -> (a rem b == a <-> abs a < abs b).
 Proof.
-intros. rewrite rem_eq, <- quot_small_iff by order.
+intros a b ?. rewrite rem_eq, <- quot_small_iff by order.
 rewrite sub_move_r, <- (add_0_r a) at 1. rewrite add_cancel_l.
 rewrite eq_sym_iff, eq_mul_0. tauto.
 Qed.
@@ -336,7 +336,7 @@ Proof. exact NZQuot.div_lt. Qed.
 
 Lemma quot_le_mono : forall a b c, 0<c -> a<=b -> a÷c <= b÷c.
 Proof.
-intros. pos_or_neg a. apply NZQuot.div_le_mono; auto.
+intros a b c **. pos_or_neg a. apply NZQuot.div_le_mono; auto.
 pos_or_neg b. apply le_trans with 0.
  rewrite <- opp_nonneg_nonpos, <- quot_opp_l by order.
  apply quot_pos; order.
@@ -350,7 +350,7 @@ Qed.
 
 Lemma mul_quot_le : forall a b, 0<=a -> b~=0 -> 0 <= b*(a÷b) <= a.
 Proof.
-intros. pos_or_neg b.
+intros a b **. pos_or_neg b.
 split.
 apply mul_nonneg_nonneg; [|apply quot_pos]; order.
 apply NZQuot.mul_div_le; order.
@@ -362,7 +362,7 @@ Qed.
 
 Lemma mul_quot_ge : forall a b, a<=0 -> b~=0 -> a <= b*(a÷b) <= 0.
 Proof.
-intros.
+intros a b **.
 rewrite <- opp_nonneg_nonpos, opp_le_mono, <-mul_opp_r, <-quot_opp_l by order.
 rewrite <- opp_nonneg_nonpos in *.
 destruct (mul_quot_le (-a) b); tauto.
@@ -415,7 +415,7 @@ Proof. exact NZQuot.div_lt_upper_bound. Qed.
 Theorem quot_le_upper_bound:
   forall a b q, 0<b -> a <= b*q -> a÷b <= q.
 Proof.
-intros.
+intros a b q **.
 rewrite <- (quot_mul q b) by order.
 apply quot_le_mono; trivial. now rewrite mul_comm.
 Qed.
@@ -423,7 +423,7 @@ Qed.
 Theorem quot_le_lower_bound:
   forall a b q, 0<b -> b*q <= a -> q <= a÷b.
 Proof.
-intros.
+intros a b q **.
 rewrite <- (quot_mul q b) by order.
 apply quot_le_mono; trivial. now rewrite mul_comm.
 Qed.
@@ -443,7 +443,7 @@ Lemma rem_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a ->
  (a + b * c) rem c == a rem c.
 Proof.
 assert (forall a b c, c~=0 -> 0<=a -> 0<=a+b*c -> (a+b*c) rem c == a rem c).
- intros. pos_or_neg c. apply NZQuot.mod_add; order.
+ intros a b c **. pos_or_neg c. apply NZQuot.mod_add; order.
  rewrite <- (rem_opp_r a), <- (rem_opp_r (a+b*c)) by order.
  rewrite <- mul_opp_opp in *.
  apply NZQuot.mod_add; order.
@@ -457,7 +457,7 @@ Qed.
 Lemma quot_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a ->
  (a + b * c) ÷ c == a ÷ c + b.
 Proof.
-intros.
+intros a b c **.
 rewrite <- (mul_cancel_l _ _ c) by trivial.
 rewrite <- (add_cancel_r _ _ ((a+b*c) rem c)).
 rewrite <- quot_rem, rem_add by trivial.
@@ -476,14 +476,14 @@ Lemma quot_mul_cancel_r : forall a b c, b~=0 -> c~=0 ->
  (a*c)÷(b*c) == a÷b.
 Proof.
 assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a*c)÷(b*c) == a÷b).
- intros. pos_or_neg c. apply NZQuot.div_mul_cancel_r; order.
+ intros a b c **. pos_or_neg c. apply NZQuot.div_mul_cancel_r; order.
  rewrite <- quot_opp_opp, <- 2 mul_opp_r. apply NZQuot.div_mul_cancel_r; order.
  rewrite <- neq_mul_0; intuition order.
 assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a*c)÷(b*c) == a÷b).
- intros. pos_or_neg b. apply Aux1; order.
+ intros a b c **. pos_or_neg b. apply Aux1; order.
  apply opp_inj. rewrite <- 2 quot_opp_r, <- mul_opp_l; try order. apply Aux1; order.
  rewrite <- neq_mul_0; intuition order.
-intros. pos_or_neg a. apply Aux2; order.
+intros a b c **. pos_or_neg a. apply Aux2; order.
 apply opp_inj. rewrite <- 2 quot_opp_l, <- mul_opp_l; try order. apply Aux2; order.
 rewrite <- neq_mul_0; intuition order.
 Qed.
@@ -491,13 +491,13 @@ Qed.
 Lemma quot_mul_cancel_l : forall a b c, b~=0 -> c~=0 ->
  (c*a)÷(c*b) == a÷b.
 Proof.
-intros. rewrite !(mul_comm c); now apply quot_mul_cancel_r.
+intros a b c **. rewrite !(mul_comm c); now apply quot_mul_cancel_r.
 Qed.
 
 Lemma mul_rem_distr_r: forall a b c, b~=0 -> c~=0 ->
   (a*c) rem (b*c) == (a rem b) * c.
 Proof.
-intros.
+intros a b c **.
 assert (b*c ~= 0) by (rewrite <- neq_mul_0; tauto).
 rewrite ! rem_eq by trivial.
 rewrite quot_mul_cancel_r by order.
@@ -507,7 +507,7 @@ Qed.
 Lemma mul_rem_distr_l: forall a b c, b~=0 -> c~=0 ->
   (c*a) rem (c*b) == c * (a rem b).
 Proof.
-intros; rewrite !(mul_comm c); now apply mul_rem_distr_r.
+intros a b c **; rewrite !(mul_comm c); now apply mul_rem_distr_r.
 Qed.
 
 (** Operations modulo. *)
@@ -515,7 +515,7 @@ Qed.
 Theorem rem_rem: forall a n, n~=0 ->
  (a rem n) rem n == a rem n.
 Proof.
-intros. pos_or_neg a; pos_or_neg n. apply NZQuot.mod_mod; order.
+intros a n **. pos_or_neg a; pos_or_neg n. apply NZQuot.mod_mod; order.
 rewrite <- ! (rem_opp_r _ n) by trivial. apply NZQuot.mod_mod; order.
 apply opp_inj. rewrite <- !rem_opp_l by order. apply NZQuot.mod_mod; order.
 apply opp_inj. rewrite <- !rem_opp_opp by order. apply NZQuot.mod_mod; order.
@@ -526,11 +526,11 @@ Lemma mul_rem_idemp_l : forall a b n, n~=0 ->
 Proof.
 assert (Aux1 : forall a b n, 0<=a -> 0<=b -> n~=0 ->
          ((a rem n)*b) rem n == (a*b) rem n).
- intros. pos_or_neg n. apply NZQuot.mul_mod_idemp_l; order.
+ intros a b n **. pos_or_neg n. apply NZQuot.mul_mod_idemp_l; order.
  rewrite <- ! (rem_opp_r _ n) by order. apply NZQuot.mul_mod_idemp_l; order.
 assert (Aux2 : forall a b n, 0<=a -> n~=0 ->
          ((a rem n)*b) rem n == (a*b) rem n).
- intros. pos_or_neg b. now apply Aux1.
+ intros a b n **. pos_or_neg b. now apply Aux1.
  apply opp_inj. rewrite <-2 rem_opp_l, <-2 mul_opp_r by order.
   apply Aux1; order.
 intros a b n Hn. pos_or_neg a. now apply Aux2.
@@ -541,7 +541,7 @@ Qed.
 Lemma mul_rem_idemp_r : forall a b n, n~=0 ->
  (a*(b rem n)) rem n == (a*b) rem n.
 Proof.
-intros. rewrite !(mul_comm a). now apply mul_rem_idemp_l.
+intros a b n **. rewrite !(mul_comm a). now apply mul_rem_idemp_l.
 Qed.
 
 Theorem mul_rem: forall a b n, n~=0 ->
@@ -564,7 +564,7 @@ Lemma add_rem_idemp_l : forall a b n, n~=0 -> 0 <= a*b ->
 Proof.
 assert (Aux : forall a b n, 0<=a -> 0<=b -> n~=0 ->
           ((a rem n)+b) rem n == (a+b) rem n).
- intros. pos_or_neg n. apply NZQuot.add_mod_idemp_l; order.
+ intros a b n **. pos_or_neg n. apply NZQuot.add_mod_idemp_l; order.
  rewrite <- ! (rem_opp_r _ n) by order. apply NZQuot.add_mod_idemp_l; order.
 intros a b n Hn Hab. destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)].
 now apply Aux.
@@ -576,7 +576,7 @@ Qed.
 Lemma add_rem_idemp_r : forall a b n, n~=0 -> 0 <= a*b ->
  (a+(b rem n)) rem n == (a+b) rem n.
 Proof.
-intros. rewrite !(add_comm a). apply add_rem_idemp_l; trivial.
+intros a b n **. rewrite !(add_comm a). apply add_rem_idemp_l; trivial.
 now rewrite mul_comm.
 Qed.
 
@@ -598,16 +598,16 @@ Lemma quot_quot : forall a b c, b~=0 -> c~=0 ->
  (a÷b)÷c == a÷(b*c).
 Proof.
 assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a÷b)÷c == a÷(b*c)).
- intros. pos_or_neg c. apply NZQuot.div_div; order.
+ intros a b c **. pos_or_neg c. apply NZQuot.div_div; order.
  apply opp_inj. rewrite <- 2 quot_opp_r, <- mul_opp_r; trivial.
  apply NZQuot.div_div; order.
  rewrite <- neq_mul_0; intuition order.
 assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a÷b)÷c == a÷(b*c)).
- intros. pos_or_neg b. apply Aux1; order.
+ intros a b c **. pos_or_neg b. apply Aux1; order.
  apply opp_inj. rewrite <- quot_opp_l, <- 2 quot_opp_r, <- mul_opp_l; trivial.
  apply Aux1; trivial.
  rewrite <- neq_mul_0; intuition order.
-intros. pos_or_neg a. apply Aux2; order.
+intros a b c **. pos_or_neg a. apply Aux2; order.
 apply opp_inj. rewrite <- 3 quot_opp_l; try order. apply Aux2; order.
 rewrite <- neq_mul_0. tauto.
 Qed.
diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v
index 09d28a18ec..755557ff17 100644
--- a/theories/Numbers/Integer/Abstract/ZGcd.v
+++ b/theories/Numbers/Integer/Abstract/ZGcd.v
@@ -98,7 +98,7 @@ Qed.
 
 Lemma gcd_abs_l : forall n m, gcd (abs n) m == gcd n m.
 Proof.
- intros. destruct (abs_eq_or_opp n) as [H|H]; rewrite H.
+ intros n m. destruct (abs_eq_or_opp n) as [H|H]; rewrite H.
  easy. apply gcd_opp_l.
 Qed.
 
@@ -125,7 +125,7 @@ Qed.
 
 Lemma gcd_add_mult_diag_r : forall n m p, gcd n (m+p*n) == gcd n m.
 Proof.
- intros. apply gcd_unique_alt; try apply gcd_nonneg.
+ intros n m p. apply gcd_unique_alt; try apply gcd_nonneg.
  intros. rewrite gcd_divide_iff. split; intros (U,V); split; trivial.
  apply divide_add_r; trivial. now apply divide_mul_r.
  apply divide_add_cancel_r with (p*n); trivial.
@@ -164,12 +164,12 @@ Proof.
  (* First, a version restricted to natural numbers *)
  assert (aux : forall n, 0<=n -> forall m, 0<=m -> Bezout n m (gcd n m)).
   intros n Hn; pattern n.
-  apply strong_right_induction with (z:=0); trivial.
+  apply (fun H => strong_right_induction _ H 0); trivial.
   unfold Bezout. solve_proper.
   clear n Hn. intros n Hn IHn.
   apply le_lteq in Hn; destruct Hn as [Hn|Hn].
   intros m Hm; pattern m.
-  apply strong_right_induction with (z:=0); trivial.
+  apply (fun H => strong_right_induction _ H 0); trivial.
   unfold Bezout. solve_proper.
   clear m Hm. intros m Hm IHm.
   destruct (lt_trichotomy n m) as [LT|[EQ|LT]].
@@ -227,7 +227,7 @@ Qed.
 Lemma gcd_mul_mono_l_nonneg :
  forall n m p, 0<=p -> gcd (p*n) (p*m) == p * gcd n m.
 Proof.
- intros. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_l.
+ intros n m p ?. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_l.
 Qed.
 
 Lemma gcd_mul_mono_r :
@@ -239,7 +239,7 @@ Qed.
 Lemma gcd_mul_mono_r_nonneg :
  forall n m p, 0<=p -> gcd (n*p) (m*p) == gcd n m * p.
 Proof.
- intros. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_r.
+ intros n m p ?. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_r.
 Qed.
 
 Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p).
diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v
index 6aa828ebfc..c45ea12868 100644
--- a/theories/Numbers/Integer/Abstract/ZLcm.v
+++ b/theories/Numbers/Integer/Abstract/ZLcm.v
@@ -33,14 +33,14 @@ Module Type ZLcmProp
 
 Lemma quot_div_nonneg : forall a b, 0<=a -> 0<b -> a÷b == a/b.
 Proof.
- intros. apply div_unique_pos with (a rem b).
+ intros a b **. apply div_unique_pos with (a rem b).
  now apply rem_bound_pos.
  apply quot_rem. order.
 Qed.
 
 Lemma rem_mod_nonneg : forall a b, 0<=a -> 0<b -> a rem b == a mod b.
 Proof.
- intros. apply mod_unique_pos with (a÷b).
+ intros a b **. apply mod_unique_pos with (a÷b).
  now apply rem_bound_pos.
  apply quot_rem. order.
 Qed.
@@ -290,7 +290,7 @@ Qed.
 Lemma lcm_divide_iff : forall n m p,
   (lcm n m | p) <-> (n | p) /\ (m | p).
 Proof.
- intros. split. split.
+ intros n m p. split. split.
  transitivity (lcm n m); trivial using divide_lcm_l.
  transitivity (lcm n m); trivial using divide_lcm_r.
  intros (H,H'). now apply lcm_least.
@@ -387,7 +387,7 @@ Qed.
 
 Lemma lcm_abs_l : forall n m, lcm (abs n) m == lcm n m.
 Proof.
- intros. destruct (abs_eq_or_opp n) as [H|H]; rewrite H.
+ intros n m. destruct (abs_eq_or_opp n) as [H|H]; rewrite H.
  easy. apply lcm_opp_l.
 Qed.
 
@@ -438,7 +438,7 @@ Qed.
 Lemma lcm_mul_mono_l_nonneg :
  forall n m p, 0<=p -> lcm (p*n) (p*m) == p * lcm n m.
 Proof.
- intros. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_l.
+ intros n m p ?. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_l.
 Qed.
 
 Lemma lcm_mul_mono_r :
@@ -450,7 +450,7 @@ Qed.
 Lemma lcm_mul_mono_r_nonneg :
  forall n m p, 0<=p -> lcm (n*p) (m*p) == lcm n m * p.
 Proof.
- intros. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_r.
+ intros n m p ?. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_r.
 Qed.
 
 Lemma gcd_1_lcm_mul : forall n m, n~=0 -> m~=0 ->
diff --git a/theories/Numbers/Integer/Abstract/ZMaxMin.v b/theories/Numbers/Integer/Abstract/ZMaxMin.v
index ed0b0c69a0..4af24b7754 100644
--- a/theories/Numbers/Integer/Abstract/ZMaxMin.v
+++ b/theories/Numbers/Integer/Abstract/ZMaxMin.v
@@ -20,133 +20,133 @@ Include ZMulOrderProp Z.
 
 (** Succ *)
 
-Lemma succ_max_distr : forall n m, S (max n m) == max (S n) (S m).
+Lemma succ_max_distr n m : S (max n m) == max (S n) (S m).
 Proof.
- intros. destruct (le_ge_cases n m);
+ destruct (le_ge_cases n m);
   [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?succ_le_mono.
 Qed.
 
-Lemma succ_min_distr : forall n m, S (min n m) == min (S n) (S m).
+Lemma succ_min_distr n m : S (min n m) == min (S n) (S m).
 Proof.
- intros. destruct (le_ge_cases n m);
+ destruct (le_ge_cases n m);
   [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?succ_le_mono.
 Qed.
 
 (** Pred *)
 
-Lemma pred_max_distr : forall n m, P (max n m) == max (P n) (P m).
+Lemma pred_max_distr n m : P (max n m) == max (P n) (P m).
 Proof.
- intros. destruct (le_ge_cases n m);
+ destruct (le_ge_cases n m);
   [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?pred_le_mono.
 Qed.
 
-Lemma pred_min_distr : forall n m, P (min n m) == min (P n) (P m).
+Lemma pred_min_distr n m : P (min n m) == min (P n) (P m).
 Proof.
- intros. destruct (le_ge_cases n m);
+ destruct (le_ge_cases n m);
   [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?pred_le_mono.
 Qed.
 
 (** Add *)
 
-Lemma add_max_distr_l : forall n m p, max (p + n) (p + m) == p + max n m.
+Lemma add_max_distr_l n m p : max (p + n) (p + m) == p + max n m.
 Proof.
- intros. destruct (le_ge_cases n m);
+ destruct (le_ge_cases n m);
   [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_l.
 Qed.
 
-Lemma add_max_distr_r : forall n m p, max (n + p) (m + p) == max n m + p.
+Lemma add_max_distr_r n m p : max (n + p) (m + p) == max n m + p.
 Proof.
- intros. destruct (le_ge_cases n m);
+ destruct (le_ge_cases n m);
   [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_r.
 Qed.
 
-Lemma add_min_distr_l : forall n m p, min (p + n) (p + m) == p + min n m.
+Lemma add_min_distr_l n m p : min (p + n) (p + m) == p + min n m.
 Proof.
- intros. destruct (le_ge_cases n m);
+ destruct (le_ge_cases n m);
   [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_l.
 Qed.
 
-Lemma add_min_distr_r : forall n m p, min (n + p) (m + p) == min n m + p.
+Lemma add_min_distr_r n m p : min (n + p) (m + p) == min n m + p.
 Proof.
- intros. destruct (le_ge_cases n m);
+ destruct (le_ge_cases n m);
   [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_r.
 Qed.
 
 (** Opp *)
 
-Lemma opp_max_distr : forall n m, -(max n m) == min (-n) (-m).
+Lemma opp_max_distr n m : -(max n m) == min (-n) (-m).
 Proof.
- intros. destruct (le_ge_cases n m).
+ destruct (le_ge_cases n m).
  rewrite max_r by trivial. symmetry. apply min_r. now rewrite <- opp_le_mono.
  rewrite max_l by trivial. symmetry. apply min_l. now rewrite <- opp_le_mono.
 Qed.
 
-Lemma opp_min_distr : forall n m, -(min n m) == max (-n) (-m).
+Lemma opp_min_distr n m : -(min n m) == max (-n) (-m).
 Proof.
- intros. destruct (le_ge_cases n m).
+ destruct (le_ge_cases n m).
  rewrite min_l by trivial. symmetry. apply max_l. now rewrite <- opp_le_mono.
  rewrite min_r by trivial. symmetry. apply max_r. now rewrite <- opp_le_mono.
 Qed.
 
 (** Sub *)
 
-Lemma sub_max_distr_l : forall n m p, max (p - n) (p - m) == p - min n m.
+Lemma sub_max_distr_l n m p : max (p - n) (p - m) == p - min n m.
 Proof.
- intros. destruct (le_ge_cases n m).
+ destruct (le_ge_cases n m).
  rewrite min_l by trivial. apply max_l. now rewrite <- sub_le_mono_l.
  rewrite min_r by trivial. apply max_r. now rewrite <- sub_le_mono_l.
 Qed.
 
-Lemma sub_max_distr_r : forall n m p, max (n - p) (m - p) == max n m - p.
+Lemma sub_max_distr_r n m p : max (n - p) (m - p) == max n m - p.
 Proof.
- intros. destruct (le_ge_cases n m);
+ destruct (le_ge_cases n m);
   [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply sub_le_mono_r.
 Qed.
 
-Lemma sub_min_distr_l : forall n m p, min (p - n) (p - m) == p - max n m.
+Lemma sub_min_distr_l n m p : min (p - n) (p - m) == p - max n m.
 Proof.
- intros. destruct (le_ge_cases n m).
+ destruct (le_ge_cases n m).
  rewrite max_r by trivial. apply min_r. now rewrite <- sub_le_mono_l.
  rewrite max_l by trivial. apply min_l. now rewrite <- sub_le_mono_l.
 Qed.
 
-Lemma sub_min_distr_r : forall n m p, min (n - p) (m - p) == min n m - p.
+Lemma sub_min_distr_r n m p : min (n - p) (m - p) == min n m - p.
 Proof.
- intros. destruct (le_ge_cases n m);
+ destruct (le_ge_cases n m);
   [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply sub_le_mono_r.
 Qed.
 
 (** Mul *)
 
-Lemma mul_max_distr_nonneg_l : forall n m p, 0 <= p ->
+Lemma mul_max_distr_nonneg_l n m p : 0 <= p ->
  max (p * n) (p * m) == p * max n m.
 Proof.
  intros. destruct (le_ge_cases n m);
   [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_nonneg_l.
 Qed.
 
-Lemma mul_max_distr_nonneg_r : forall n m p, 0 <= p ->
+Lemma mul_max_distr_nonneg_r n m p : 0 <= p ->
  max (n * p) (m * p) == max n m * p.
 Proof.
  intros. destruct (le_ge_cases n m);
   [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_nonneg_r.
 Qed.
 
-Lemma mul_min_distr_nonneg_l : forall n m p, 0 <= p ->
+Lemma mul_min_distr_nonneg_l n m p : 0 <= p ->
  min (p * n) (p * m) == p * min n m.
 Proof.
  intros. destruct (le_ge_cases n m);
   [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_nonneg_l.
 Qed.
 
-Lemma mul_min_distr_nonneg_r : forall n m p, 0 <= p ->
+Lemma mul_min_distr_nonneg_r n m p : 0 <= p ->
  min (n * p) (m * p) == min n m * p.
 Proof.
  intros. destruct (le_ge_cases n m);
   [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_nonneg_r.
 Qed.
 
-Lemma mul_max_distr_nonpos_l : forall n m p, p <= 0 ->
+Lemma mul_max_distr_nonpos_l n m p : p <= 0 ->
  max (p * n) (p * m) == p * min n m.
 Proof.
  intros. destruct (le_ge_cases n m).
@@ -154,7 +154,7 @@ Proof.
  rewrite min_r by trivial. rewrite max_r. reflexivity. now apply mul_le_mono_nonpos_l.
 Qed.
 
-Lemma mul_max_distr_nonpos_r : forall n m p, p <= 0 ->
+Lemma mul_max_distr_nonpos_r n m p : p <= 0 ->
  max (n * p) (m * p) == min n m * p.
 Proof.
  intros. destruct (le_ge_cases n m).
@@ -162,7 +162,7 @@ Proof.
  rewrite min_r by trivial. rewrite max_r. reflexivity. now apply mul_le_mono_nonpos_r.
 Qed.
 
-Lemma mul_min_distr_nonpos_l : forall n m p, p <= 0 ->
+Lemma mul_min_distr_nonpos_l n m p : p <= 0 ->
  min (p * n) (p * m) == p * max n m.
 Proof.
  intros. destruct (le_ge_cases n m).
@@ -170,7 +170,7 @@ Proof.
  rewrite max_l by trivial. rewrite min_l. reflexivity. now apply mul_le_mono_nonpos_l.
 Qed.
 
-Lemma mul_min_distr_nonpos_r : forall n m p, p <= 0 ->
+Lemma mul_min_distr_nonpos_r n m p : p <= 0 ->
  min (n * p) (m * p) == max n m * p.
 Proof.
  intros. destruct (le_ge_cases n m).
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index 7d97d11818..0275a5fa65 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -167,7 +167,7 @@ Qed.
 Theorem eq_mul_1 : forall n m, n * m == 1 -> n == 1 \/ n == -1.
 Proof.
 assert (F := lt_m1_0).
-zero_pos_neg n.
+intro n; zero_pos_neg n.
 (* n = 0 *)
 intros m. nzsimpl. now left.
 (* 0 < n, proving P n /\ P (-n) *)
@@ -205,7 +205,7 @@ Qed.
 
 Theorem lt_mul_r : forall n m p, 0 < n -> 1 < p -> n < m -> n < m * p.
 Proof.
-intros. stepl (n * 1) by now rewrite mul_1_r.
+intros n m p **. stepl (n * 1) by now rewrite mul_1_r.
 apply mul_lt_mono_nonneg.
 now apply lt_le_incl. assumption. apply le_0_1. assumption.
 Qed.
diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v
index 4b61b18479..0f68278cf0 100644
--- a/theories/Numbers/Integer/Abstract/ZParity.v
+++ b/theories/Numbers/Integer/Abstract/ZParity.v
@@ -19,19 +19,19 @@ Include NZParityProp Z Z ZP.
 
 Lemma odd_pred : forall n, odd (P n) = even n.
 Proof.
- intros. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ.
+ intros n. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ.
 Qed.
 
 Lemma even_pred : forall n, even (P n) = odd n.
 Proof.
- intros. rewrite <- (succ_pred n) at 2. symmetry. apply odd_succ.
+ intros n. rewrite <- (succ_pred n) at 2. symmetry. apply odd_succ.
 Qed.
 
 Lemma even_opp : forall n, even (-n) = even n.
 Proof.
  assert (H : forall n, Even n -> Even (-n)).
   intros n (m,H). exists (-m). rewrite mul_opp_r. now f_equiv.
- intros. rewrite eq_iff_eq_true, !even_spec.
+ intros n. rewrite eq_iff_eq_true, !even_spec.
  split. rewrite <- (opp_involutive n) at 2. apply H.
  apply H.
 Qed.
diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v
index bec77fd136..9557212a86 100644
--- a/theories/Numbers/Integer/Abstract/ZPow.v
+++ b/theories/Numbers/Integer/Abstract/ZPow.v
@@ -73,7 +73,7 @@ Qed.
 
 Lemma pow_even_abs : forall a b, Even b -> a^b == (abs a)^b.
 Proof.
- intros. destruct (abs_eq_or_opp a) as [EQ|EQ]; rewrite EQ.
+ intros a b ?. destruct (abs_eq_or_opp a) as [EQ|EQ]; rewrite EQ.
  reflexivity.
  symmetry. now apply pow_opp_even.
 Qed.
@@ -119,7 +119,7 @@ Qed.
 Lemma abs_pow : forall a b, abs (a^b) == (abs a)^b.
 Proof.
  intros a b.
- destruct (Even_or_Odd b).
+ destruct (Even_or_Odd b) as [H|H].
  rewrite pow_even_abs by trivial.
  apply abs_eq, pow_nonneg, abs_nonneg.
  rewrite pow_odd_abs_sgn by trivial.
diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v
index 03e0c0345d..3ebbec9397 100644
--- a/theories/Numbers/Integer/Abstract/ZSgnAbs.v
+++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.v
@@ -40,11 +40,11 @@ Module Type GenericSgn (Import Z : ZDecAxiomsSig')
                        (Import ZP : ZMulOrderProp Z) <: HasSgn Z.
  Definition sgn n :=
   match compare 0 n with Eq => 0 | Lt => 1 | Gt => -1 end.
- Lemma sgn_null : forall n, n==0 -> sgn n == 0.
+ Lemma sgn_null n : n==0 -> sgn n == 0.
  Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed.
- Lemma sgn_pos : forall n, 0<n -> sgn n == 1.
+ Lemma sgn_pos n : 0<n -> sgn n == 1.
  Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed.
- Lemma sgn_neg : forall n, n<0 -> sgn n == -1.
+ Lemma sgn_neg n : n<0 -> sgn n == -1.
  Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed.
 End GenericSgn.
 
@@ -101,7 +101,7 @@ Qed.
 
 Lemma abs_opp : forall n, abs (-n) == abs n.
 Proof.
- intros. destruct_max n.
+ intros n. destruct_max n.
  rewrite (abs_neq (-n)), opp_involutive. reflexivity.
  now rewrite opp_nonpos_nonneg.
  rewrite (abs_eq (-n)). reflexivity.
@@ -115,14 +115,14 @@ Qed.
 
 Lemma abs_0_iff : forall n, abs n == 0 <-> n==0.
 Proof.
- split. destruct_max n; auto.
+ intros n; split. destruct_max n; auto.
  now rewrite eq_opp_l, opp_0.
  intros EQ; rewrite EQ. rewrite abs_eq; auto using eq_refl, le_refl.
 Qed.
 
 Lemma abs_pos : forall n, 0 < abs n <-> n~=0.
 Proof.
- intros. rewrite <- abs_0_iff. split; [intros LT| intros NEQ].
+ intros n. rewrite <- abs_0_iff. split; [intros LT| intros NEQ].
  intro EQ. rewrite EQ in LT. now elim (lt_irrefl 0).
  assert (LE : 0 <= abs n) by apply abs_nonneg.
  rewrite lt_eq_cases in LE; destruct LE; auto.
@@ -131,12 +131,12 @@ Qed.
 
 Lemma abs_eq_or_opp : forall n, abs n == n \/ abs n == -n.
 Proof.
- intros. destruct_max n; auto with relations.
+ intros n. destruct_max n; auto with relations.
 Qed.
 
 Lemma abs_or_opp_abs : forall n, n == abs n \/ n == - abs n.
 Proof.
- intros. destruct_max n; rewrite ? opp_involutive; auto with relations.
+ intros n. destruct_max n; rewrite ? opp_involutive; auto with relations.
 Qed.
 
 Lemma abs_involutive : forall n, abs (abs n) == abs n.
@@ -147,7 +147,7 @@ Qed.
 Lemma abs_spec : forall n,
   (0 <= n /\ abs n == n) \/ (n < 0 /\ abs n == -n).
 Proof.
- intros. destruct (le_gt_cases 0 n).
+ intros n. destruct (le_gt_cases 0 n).
  left; split; auto. now apply abs_eq.
  right; split; auto. apply abs_neq. now apply lt_le_incl.
 Qed.
@@ -156,7 +156,7 @@ Lemma abs_case_strong :
   forall (P:t->Prop) n, Proper (eq==>iff) P ->
     (0<=n -> P n) -> (n<=0 -> P (-n)) -> P (abs n).
 Proof.
- intros. destruct_max n; auto.
+ intros P n **. destruct_max n; auto.
 Qed.
 
 Lemma abs_case : forall (P:t->Prop) n, Proper (eq==>iff) P ->
@@ -196,7 +196,7 @@ Qed.
 
 Lemma abs_triangle : forall n m, abs (n + m) <= abs n + abs m.
 Proof.
- intros. destruct_max n; destruct_max m.
+ intros n m. destruct_max n; destruct_max m.
  rewrite abs_eq. apply le_refl. now apply add_nonneg_nonneg.
  destruct_max (n+m); try rewrite opp_add_distr;
   apply add_le_mono_l || apply add_le_mono_r.
@@ -212,7 +212,7 @@ Qed.
 
 Lemma abs_sub_triangle : forall n m, abs n - abs m <= abs (n-m).
 Proof.
- intros.
+ intros n m.
  rewrite le_sub_le_add_l, add_comm.
  rewrite <- (sub_simpl_r n m) at 1.
  apply abs_triangle.
@@ -223,10 +223,10 @@ Qed.
 Lemma abs_mul : forall n m, abs (n * m) == abs n * abs m.
 Proof.
  assert (H : forall n m, 0<=n -> abs (n*m) == n * abs m).
-  intros. destruct_max m.
+  intros n m ?. destruct_max m.
   rewrite abs_eq. apply eq_refl. now apply mul_nonneg_nonneg.
   rewrite abs_neq, mul_opp_r. reflexivity. now apply mul_nonneg_nonpos .
- intros. destruct_max n. now apply H.
+ intros n m. destruct_max n. now apply H.
  rewrite <- mul_opp_opp, H, abs_opp. reflexivity.
  now apply opp_nonneg_nonpos.
 Qed.
@@ -271,7 +271,7 @@ Qed.
 
 Lemma sgn_pos_iff : forall n, sgn n == 1 <-> 0<n.
 Proof.
- split; try apply sgn_pos. destruct_sgn n; auto.
+ intros n; split; try apply sgn_pos. destruct_sgn n; auto.
  intros. elim (lt_neq 0 1); auto. apply lt_0_1.
  intros. elim (lt_neq (-1) 1); auto.
  apply lt_trans with 0. rewrite opp_neg_pos. apply lt_0_1. apply lt_0_1.
@@ -279,7 +279,7 @@ Qed.
 
 Lemma sgn_null_iff : forall n, sgn n == 0 <-> n==0.
 Proof.
- split; try apply sgn_null. destruct_sgn n; auto with relations.
+ intros n; split; try apply sgn_null. destruct_sgn n; auto with relations.
  intros. elim (lt_neq 0 1); auto with relations. apply lt_0_1.
  intros. elim (lt_neq (-1) 0); auto.
  rewrite opp_neg_pos. apply lt_0_1.
@@ -287,7 +287,7 @@ Qed.
 
 Lemma sgn_neg_iff : forall n, sgn n == -1 <-> n<0.
 Proof.
- split; try apply sgn_neg. destruct_sgn n; auto with relations.
+ intros n; split; try apply sgn_neg. destruct_sgn n; auto with relations.
  intros. elim (lt_neq (-1) 1); auto with relations.
  apply lt_trans with 0. rewrite opp_neg_pos. apply lt_0_1. apply lt_0_1.
  intros. elim (lt_neq (-1) 0); auto with relations.
@@ -296,7 +296,7 @@ Qed.
 
 Lemma sgn_opp : forall n, sgn (-n) == - sgn n.
 Proof.
- intros. destruct_sgn n.
+ intros n. destruct_sgn n.
  apply sgn_neg. now rewrite opp_neg_pos.
  setoid_replace n with 0 by auto with relations.
   rewrite opp_0. apply sgn_0.
@@ -305,7 +305,7 @@ Qed.
 
 Lemma sgn_nonneg : forall n, 0 <= sgn n <-> 0 <= n.
 Proof.
- split.
+ intros n; split.
  destruct_sgn n; intros.
  now apply lt_le_incl.
  order.
@@ -323,7 +323,7 @@ Qed.
 
 Lemma sgn_mul : forall n m, sgn (n*m) == sgn n * sgn m.
 Proof.
- intros. destruct_sgn n; nzsimpl.
+ intros n m. destruct_sgn n; nzsimpl.
  destruct_sgn m.
   apply sgn_pos. now apply mul_pos_pos.
   apply sgn_null. rewrite eq_mul_0; auto with relations.
@@ -337,7 +337,7 @@ Qed.
 
 Lemma sgn_abs : forall n, n * sgn n == abs n.
 Proof.
- intros. symmetry.
+ intros n. symmetry.
  destruct_sgn n; try rewrite mul_opp_r; nzsimpl.
  apply abs_eq. now apply lt_le_incl.
  rewrite abs_0_iff; auto with relations.
@@ -346,7 +346,7 @@ Qed.
 
 Lemma abs_sgn : forall n, abs n * sgn n == n.
 Proof.
- intros.
+ intros n.
  destruct_sgn n; try rewrite mul_opp_r; nzsimpl; auto.
  apply abs_eq. now apply lt_le_incl.
  rewrite eq_opp_l. apply abs_neq. now apply lt_le_incl.
@@ -354,7 +354,7 @@ Qed.
 
 Lemma sgn_sgn : forall x, sgn (sgn x) == sgn x.
 Proof.
- intros.
+ intros x.
  destruct (sgn_spec x) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ.
  apply sgn_pos, lt_0_1.
  now apply sgn_null.