Merge PR #12905: Lint stdlib with -mangle-names #2

Reviewed-by: anton-trunov
Ack-by: jashug
Ack-by: olaure01

26 files changed, 188 insertions, 168 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 9e10786fcd..0f62db42cf 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -258,7 +258,7 @@ Qed.
 Lemma orb_true_elim :
   forall b1 b2:bool, b1 || b2 = true -> {b1 = true} + {b2 = true}.
 Proof.
-  destruct b1; simpl; auto.
+  intro b1; destruct b1; simpl; auto.
 Defined.
 
 Lemma orb_prop : forall a b:bool, a || b = true -> a = true \/ b = true.
@@ -424,7 +424,7 @@ Notation andb_true_b := andb_true_l (only parsing).
 Lemma andb_false_elim :
   forall b1 b2:bool, b1 && b2 = false -> {b1 = false} + {b2 = false}.
 Proof.
-  destruct b1; simpl; auto.
+  intro b1; destruct b1; simpl; auto.
 Defined.
 Hint Resolve andb_false_elim: bool.
 
@@ -681,17 +681,17 @@ Qed.
 
 Lemma negb_xorb_l : forall b b', negb (xorb b b') = xorb (negb b) b'.
 Proof.
- destruct b,b'; trivial.
+  intros b b'; destruct b,b'; trivial.
 Qed.
 
 Lemma negb_xorb_r : forall b b', negb (xorb b b') = xorb b (negb b').
 Proof.
- destruct b,b'; trivial.
+  intros b b'; destruct b,b'; trivial.
 Qed.
 
 Lemma xorb_negb_negb : forall b b', xorb (negb b) (negb b') = xorb b b'.
 Proof.
- destruct b,b'; trivial.
+  intros b b'; destruct b,b'; trivial.
 Qed.
 
 (** Lemmas about the [b = true] embedding of [bool] to [Prop] *)
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 598bd8b9c5..9a3a1d3709 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -20,7 +20,7 @@ Require Import Coq.Program.Tactics.
 Require Export Coq.Classes.CRelationClasses.
 
 Generalizable Variables A eqA B C D R RA RB RC m f x y.
-Local Obligation Tactic := simpl_crelation.
+Local Obligation Tactic := try solve [ simpl_crelation ].
 
 Set Universe Polymorphism.
 
@@ -268,6 +268,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros A R H B R' H0 x y z X X0 x0 y0 X1.
     assert(R x0 x0).
     - transitivity y0... symmetry...
     - transitivity (y x0)...
@@ -284,6 +285,7 @@ Section GenericInstances.
   
   Next Obligation.
   Proof.
+    intros A B C RA RB RC f mor x y X x0 y0 X0.
     apply mor ; auto.
   Qed.
 
@@ -297,6 +299,7 @@ Section GenericInstances.
   
   Next Obligation.
   Proof with auto.
+    intros A R H x y X x0 y0 X0 X1.
     transitivity x...
     transitivity x0...
   Qed.
@@ -309,6 +312,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros A R H x x0 y X X0.
     transitivity y...
   Qed.
 
@@ -318,6 +322,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros A R H x x0 y X X0.
     transitivity x0...
   Qed.
 
@@ -327,6 +332,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros A R H x x0 y X X0.
     transitivity y... symmetry...
   Qed.
 
@@ -335,6 +341,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros A R H x x0 y X X0.
     transitivity x0... symmetry...
   Qed.
 
@@ -343,6 +350,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros A R H x x0 y X.
     split.
     - intros ; transitivity x0...
     - intros.
@@ -358,6 +366,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros A R H x y X y0 y1 e X0; destruct e.
     transitivity y...
   Qed.
 
@@ -368,6 +377,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros A R H x y X x0 y0 X0.
     split ; intros.
     - transitivity x0... transitivity x... symmetry...
 
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index a27919dd43..72a196ca7a 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -319,7 +319,7 @@ Section Binary.
     split; red; unfold relation_equivalence, iffT.
     - firstorder.
     - firstorder.
-    - intros. specialize (X x0 y0). specialize (X0 x0 y0). firstorder.
+    - intros x y z X X0 x0 y0. specialize (X x0 y0). specialize (X0 x0 y0). firstorder.
   Qed.
     
   Global Instance relation_implication_preorder : PreOrder (@subrelation A).
@@ -346,7 +346,7 @@ Section Binary.
   Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R).
   Proof.
     unfold flip; constructor; unfold flip.
-    - intros. apply H. apply symmetry. apply X.
+    - intros X. apply H. apply symmetry. apply X.
     - unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption.
   Qed.
 End Binary.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 43adb0b69f..c70e3fe478 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -21,7 +21,7 @@ Require Import Coq.Relations.Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 
 Generalizable Variables A eqA B C D R RA RB RC m f x y.
-Local Obligation Tactic := simpl_relation.
+Local Obligation Tactic := try solve [ simpl_relation ].
 
 (** * Morphisms.
 
@@ -201,12 +201,12 @@ Section Relations.
 
   Global Instance pointwise_subrelation `(sub : subrelation B R R') :
     subrelation (pointwise_relation R) (pointwise_relation R') | 4.
-  Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
+  Proof. intros x y H a. unfold pointwise_relation in *. apply sub. apply H. Qed.
   
   (** For dependent function types. *)
   Lemma forall_subrelation (R S : forall x : A, relation (P x)) :
     (forall a, subrelation (R a) (S a)) -> subrelation (forall_relation R) (forall_relation S).
-  Proof. reduce. apply H. apply H0. Qed.
+  Proof. intros H x y H0 a. apply H. apply H0. Qed.
 End Relations.
 
 Typeclasses Opaque respectful pointwise_relation forall_relation.
@@ -259,6 +259,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros R H R' H0 x y z H1 H2 x0 y0 H3.
     assert(R x0 x0).
     - transitivity y0... symmetry...
     - transitivity (y x0)...
@@ -272,6 +273,7 @@ Section GenericInstances.
   
   Next Obligation.
   Proof.
+    intros RA R mR x y H x0 y0 H0.
     unfold complement.
     pose (mR x y H x0 y0 H0).
     intuition.
@@ -285,7 +287,7 @@ Section GenericInstances.
   
   Next Obligation.
   Proof.
-    apply mor ; auto.
+    intros RA RB RC f mor x y H x0 y0 H0; apply mor ; auto.
   Qed.
 
 
@@ -298,6 +300,7 @@ Section GenericInstances.
   
   Next Obligation.
   Proof with auto.
+    intros R H x y H0 x0 y0 H1 H2.
     transitivity x...
     transitivity x0...
   Qed.
@@ -310,6 +313,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros R H x x0 y H0 H1.
     transitivity y...
   Qed.
 
@@ -319,6 +323,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros R H x x0 y H0 H1.
     transitivity x0...
   Qed.
 
@@ -328,6 +333,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros R H x x0 y H0 H1.
     transitivity y... symmetry...
   Qed.
 
@@ -336,6 +342,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros R H x x0 y H0 H1.
     transitivity x0... symmetry...
   Qed.
 
@@ -344,6 +351,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros R H x x0 y H0.
     split.
     - intros ; transitivity x0...
     - intros.
@@ -359,6 +367,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros R H x y H0 y0 y1 e H2; destruct e.
     transitivity y...
   Qed.
 
@@ -369,6 +378,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
+    intros R H x y H0 x0 y0 H1.
     split ; intros.
     - transitivity x0... transitivity x... symmetry...
 
@@ -383,7 +393,7 @@ Section GenericInstances.
 
   Next Obligation.
   Proof.
-    simpl_relation.
+    intros RA RB RC x y H x0 y0 H0 x1 y1 H1.
     unfold compose. apply H. apply H0. apply H1.
   Qed.
 
@@ -400,9 +410,9 @@ Section GenericInstances.
     Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) 
            (@respectful A B).
   Proof.
-    reduce.
+    intros x y H x0 y0 H0 x1 x2.
     unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
-    split ; intros.
+    split ; intros H1 x3 y1 H2.
     
     - rewrite <- H0.
       apply H1.
@@ -512,9 +522,9 @@ Ltac partial_application_tactic :=
 
 Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).
 Proof.
-  simpl_relation.
+  intros A x y H y0 y1 e; destruct e.
   reduce in H.
-  split ; red ; intros.
+  split ; red ; intros H0.
   - setoid_rewrite <- H.
     apply H0.
   - setoid_rewrite H.
@@ -555,8 +565,7 @@ Section Normalize.
 
   Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m.
   Proof.
-    red in H, H0.
-    rewrite H.
+    rewrite normalizes.
     assumption.
   Qed.
 
@@ -571,10 +580,11 @@ Lemma flip_arrow {A : Type} {B : Type}
       `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) :
   Normalizes (A -> B) (R ==> R') (flip (R''' ==> R'')%signature).
 Proof. 
-  unfold Normalizes in *. intros.
+  unfold Normalizes in *.
   unfold relation_equivalence in *. 
   unfold predicate_equivalence in *. simpl in *.
-  unfold respectful. unfold flip in *. firstorder.
+  unfold respectful. unfold flip in *.
+  intros x x0; split; intros H x1 y H0.
   - apply NB. apply H. apply NA. apply H0.
   - apply NB. apply H. apply NA. apply H0.
 Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 9b92ade096..5381e91997 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -107,7 +107,7 @@ Section Defs.
   (** Any symmetric relation is equal to its inverse. *)
   
   Lemma subrelation_symmetric R `(Symmetric R) : subrelation (flip R) R.
-  Proof. hnf. intros. red in H0. apply symmetry. assumption. Qed.
+  Proof. hnf. intros x y H0. red in H0. apply symmetry. assumption. Qed.
 
   Section flip.
   
@@ -212,7 +212,7 @@ Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_insta
 Hint Extern 4 (subrelation (flip _) _) => 
   class_apply @subrelation_symmetric : typeclass_instances.
 
-Arguments irreflexivity {A R Irreflexive} [x] _.
+Arguments irreflexivity {A R Irreflexive} [x] _ : rename.
 Arguments symmetry {A} {R} {_} [x] [y] _.
 Arguments asymmetry {A} {R} {_} [x] [y] _ _.
 Arguments transitivity {A} {R} {_} [x] [y] [z] _ _.
@@ -260,7 +260,7 @@ Ltac simpl_relation :=
   unfold flip, impl, arrow ; try reduce ; program_simpl ;
     try ( solve [ dintuition ]).
 
-Local Obligation Tactic := simpl_relation.
+Local Obligation Tactic := try solve [ simpl_relation ].
 
 (** Logical implication. *)
 
@@ -399,29 +399,30 @@ Program Instance predicate_equivalence_equivalence :
   Equivalence (@predicate_equivalence l).
 
   Next Obligation.
-    induction l ; firstorder.
+    intro l; induction l ; firstorder.
   Qed.
   Next Obligation.
-    induction l ; firstorder.
+    intro l; induction l ; firstorder.
   Qed.
   Next Obligation.
+    intro l.
     fold pointwise_lifting.
-    induction l.
+    induction l as [|T l IHl].
     - firstorder.
-    - intros. simpl in *. pose (IHl (x x0) (y x0) (z x0)).
+    - intros x y z H H0 x0. pose (IHl (x x0) (y x0) (z x0)).
       firstorder.
   Qed.
 
 Program Instance predicate_implication_preorder :
   PreOrder (@predicate_implication l).
   Next Obligation.
-    induction l ; firstorder.
+    intro l; induction l ; firstorder.
   Qed.
   Next Obligation.
-    induction l.
+    intro l.
+    induction l as [|T l IHl].
     - firstorder.
-    - unfold predicate_implication in *. simpl in *.
-      intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.
+    - intros x y z H H0 x0. pose (IHl (x x0) (y x0) (z x0)). firstorder.
   Qed.
 
 (** We define the various operations which define the algebra on binary relations,
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 02903643d4..98fd52f351 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -77,7 +77,7 @@ Hint Resolve O_S: core.
 
 Theorem n_Sn : forall n:nat, n <> S n.
 Proof.
-  induction n; auto.
+  intro n; induction n; auto.
 Qed.
 Hint Resolve n_Sn: core.
 
@@ -92,7 +92,7 @@ Hint Resolve f_equal2_nat: core.
 
 Lemma plus_n_O : forall n:nat, n = n + 0.
 Proof.
-  induction n; simpl; auto.
+  intro n; induction n; simpl; auto.
 Qed.
 
 Remove Hints eq_refl : core.
@@ -129,13 +129,13 @@ Hint Resolve f_equal2_mult: core.
 
 Lemma mult_n_O : forall n:nat, 0 = n * 0.
 Proof.
-  induction n; simpl; auto.
+  intro n; induction n; simpl; auto.
 Qed.
 Hint Resolve mult_n_O: core.
 
 Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
 Proof.
-  intros; induction n as [| p H]; simpl; auto.
+  intros n m; induction n as [| p H]; simpl; auto.
   destruct H; rewrite <- plus_n_Sm; apply eq_S.
   pattern m at 1 3; elim m; simpl; auto.
 Qed.
@@ -192,7 +192,7 @@ Register gt as num.nat.gt.
 
 Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
 Proof.
-induction 1; auto. destruct m; simpl; auto.
+induction 1 as [|m _]; auto. destruct m; simpl; auto.
 Qed.
 
 Theorem le_S_n : forall n m, S n <= S m -> n <= m.
@@ -202,7 +202,7 @@ Qed.
 
 Theorem le_0_n : forall n, 0 <= n.
 Proof.
- induction n; constructor; trivial.
+ intro n; induction n; constructor; trivial.
 Qed.
 
 Theorem le_n_S : forall n m, n <= m -> S n <= S m.
@@ -215,7 +215,7 @@ Qed.
 Theorem nat_case :
  forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
 Proof.
-  induction n; auto.
+  intros n P IH0 IHS; case n; auto.
 Qed.
 
 (** Principle of double induction *)
@@ -226,8 +226,9 @@ Theorem nat_double_ind :
    (forall n:nat, R (S n) 0) ->
    (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.
 Proof.
+  intros R ? ? ? n.
   induction n; auto.
-  destruct m; auto.
+  intro m; destruct m; auto.
 Qed.
 
 (** Maximum and minimum : definitions and specifications *)
@@ -237,28 +238,28 @@ Notation min := Nat.min (only parsing).
 
 Lemma max_l n m : m <= n -> Nat.max n m = n.
 Proof.
- revert m; induction n; destruct m; simpl; trivial.
+ revert m; induction n as [|n IHn]; intro m; destruct m; simpl; trivial.
  - inversion 1.
  - intros. apply f_equal, IHn, le_S_n; trivial.
 Qed.
 
 Lemma max_r n m : n <= m -> Nat.max n m = m.
 Proof.
- revert m; induction n; destruct m; simpl; trivial.
+ revert m; induction n as [|n IHn]; intro m; destruct m; simpl; trivial.
  - inversion 1.
  - intros. apply f_equal, IHn, le_S_n; trivial.
 Qed.
 
 Lemma min_l n m : n <= m -> Nat.min n m = n.
 Proof.
- revert m; induction n; destruct m; simpl; trivial.
+ revert m; induction n as [|n IHn]; intro m; destruct m; simpl; trivial.
  - inversion 1.
  - intros. apply f_equal, IHn, le_S_n; trivial.
 Qed.
 
 Lemma min_r n m : m <= n -> Nat.min n m = m.
 Proof.
- revert m; induction n; destruct m; simpl; trivial.
+ revert m; induction n as [|n IHn]; intro m; destruct m; simpl; trivial.
  - inversion 1.
  - intros. apply f_equal, IHn, le_S_n; trivial.
 Qed.
@@ -267,7 +268,7 @@ Qed.
 Lemma nat_rect_succ_r {A} (f: A -> A) (x:A) n :
   nat_rect (fun _ => A) x (fun _ => f) (S n) = nat_rect (fun _ => A) (f x) (fun _ => f) n.
 Proof.
-  induction n; intros; simpl; rewrite <- ?IHn; trivial.
+  induction n as [|n IHn]; intros; simpl; rewrite <- ?IHn; trivial.
 Qed.
 
 Theorem nat_rect_plus :
@@ -275,5 +276,5 @@ Theorem nat_rect_plus :
     nat_rect (fun _ => A) x (fun _ => f) (n + m) =
       nat_rect (fun _ => A) (nat_rect (fun _ => A) x (fun _ => f) m) (fun _ => f) n.
 Proof.
-  induction n; intros; simpl; rewrite ?IHn; trivial.
+  intro n; induction n as [|n IHn]; intros; simpl; rewrite ?IHn; trivial.
 Qed.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index b13206db94..e1db68aea9 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -135,8 +135,8 @@ lazymatch T with
    rename H2 into H; find_equiv H |
    clear H]
 | forall x : ?t, _ =>
-  let a := fresh "a" with
-      H1 := fresh "H" in
+  let a := fresh "a" in
+  let H1 := fresh "H" in
     evar (a : t); pose proof (H a) as H1; unfold a in H1;
     clear a; clear H; rename H1 into H; find_equiv H
 | ?A <-> ?B => idtac
@@ -203,7 +203,7 @@ Set Implicit Arguments.
 Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}),
   C -> forall P:{C}+{~C}->Prop, (forall H:C, P (left _ H)) -> P decide.
 Proof.
-  intros; destruct decide.
+  intros C decide H P H0; destruct decide.
   - apply H0.
   - contradiction.
 Qed.
@@ -211,7 +211,7 @@ Qed.
 Lemma decide_right : forall (C:Prop) (decide:{C}+{~C}),
   ~C -> forall P:{C}+{~C}->Prop, (forall H:~C, P (right _ H)) -> P decide.
 Proof.
-  intros; destruct decide.
+  intros C decide H P H0; destruct decide.
   - contradiction.
   - apply H0.
 Qed.
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index a305626eb3..60200ae0f6 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -85,8 +85,7 @@ Section Well_founded.
 
   Scheme Acc_inv_dep := Induction for Acc Sort Prop.
 
-  Lemma Fix_F_eq :
-   forall (x:A) (r:Acc x),
+  Lemma Fix_F_eq (x:A) (r:Acc x) :
      F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)) = Fix_F (x:=x) r.
   Proof.
    destruct r using Acc_inv_dep; auto.
@@ -104,7 +103,7 @@ Section Well_founded.
 
   Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
   Proof.
-   intro x; induction (Rwf x); intros.
+   intro x; induction (Rwf x); intros r s.
    rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
    apply F_ext; auto.
   Qed.
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index 7982411bdd..66cbba9e08 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -22,7 +22,7 @@ Ltac nzsimpl' := autorewrite with nz nz'.
 
 Theorem add_0_r : forall n, n + 0 == n.
 Proof.
-  nzinduct n.
+  intro n; nzinduct n.
   - now nzsimpl.
   - intro. nzsimpl. now rewrite succ_inj_wd.
 Qed.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 8bc393bbad..d4f70adbc5 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -74,7 +74,7 @@ Proof.
 intros z Base Step; revert Base; pattern z; apply bi_induction.
 - solve_proper.
 - intro; now apply bi_induction.
-- intro; pose proof (Step n); tauto.
+- intro n; pose proof (Step n); tauto.
 Qed.
 
 End CentralInduction.
@@ -83,7 +83,7 @@ Tactic Notation "nzinduct" ident(n) :=
   induction_maker n ltac:(apply bi_induction).
 
 Tactic Notation "nzinduct" ident(n) constr(u) :=
-  induction_maker n ltac:(apply central_induction with (z := u)).
+  induction_maker n ltac:(apply (fun A A_wd => central_induction A A_wd u)).
 
 End NZBaseProp.
 
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 1c45aa440f..e6249be8df 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -116,7 +116,7 @@ Qed.
 
 Theorem div_small: forall a b, 0<=a<b -> a/b == 0.
 Proof.
-intros. symmetry.
+intros a b ?. symmetry.
 apply div_unique with a; intuition; try order.
 now nzsimpl.
 Qed.
@@ -149,7 +149,7 @@ Qed.
 
 Lemma mod_1_r: forall a, 0<=a -> a mod 1 == 0.
 Proof.
-intros. symmetry.
+intros a ?. symmetry.
 apply mod_unique with a; try split; try order; try apply lt_0_1.
 now nzsimpl.
 Qed.
@@ -173,7 +173,7 @@ Qed.
 
 Lemma mod_mul : forall a b, 0<=a -> 0<b -> (a*b) mod b == 0.
 Proof.
-intros; symmetry.
+intros a b ? ?; symmetry.
 apply mod_unique with a; try split; try order.
 - apply mul_nonneg_nonneg; order.
 - nzsimpl; apply mul_comm.
@@ -186,7 +186,7 @@ Qed.
 
 Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a.
 Proof.
-intros. destruct (le_gt_cases b a).
+intros a b ? ?. destruct (le_gt_cases b a).
 - apply le_trans with b; auto.
   apply lt_le_incl. destruct (mod_bound_pos a b); auto.
 - rewrite lt_eq_cases; right.
@@ -198,7 +198,7 @@ Qed.
 
 Lemma div_pos: forall a b, 0<=a -> 0<b -> 0 <= a/b.
 Proof.
-intros.
+intros a b ? ?.
 rewrite (mul_le_mono_pos_l _ _ b); auto; nzsimpl.
 rewrite (add_le_mono_r _ _ (a mod b)).
 rewrite <- div_mod by order.
@@ -247,7 +247,7 @@ Qed.
 
 Lemma div_lt : forall a b, 0<a -> 1<b -> a/b < a.
 Proof.
-intros.
+intros a b ? ?.
 assert (0 < b) by (apply lt_trans with 1; auto using lt_0_1).
 destruct (lt_ge_cases a b).
 - rewrite div_small; try split; order.
@@ -284,7 +284,7 @@ Qed.
 
 Lemma mul_div_le : forall a b, 0<=a -> 0<b -> b*(a/b) <= a.
 Proof.
-intros.
+intros a b ? ?.
 rewrite (add_le_mono_r _ _ (a mod b)), <- div_mod by order.
 rewrite <- (add_0_r a) at 1.
 rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order.
@@ -292,7 +292,7 @@ Qed.
 
 Lemma mul_succ_div_gt : forall a b, 0<=a -> 0<b -> a < b*(S (a/b)).
 Proof.
-intros.
+intros a b ? ?.
 rewrite (div_mod a b) at 1 by order.
 rewrite (mul_succ_r).
 rewrite <- add_lt_mono_l.
@@ -304,7 +304,7 @@ Qed.
 
 Lemma div_exact : forall a b, 0<=a -> 0<b -> (a == b*(a/b) <-> a mod b == 0).
 Proof.
-intros. rewrite (div_mod a b) at 1 by order.
+intros a b ? ?. rewrite (div_mod a b) at 1 by order.
 rewrite <- (add_0_r (b*(a/b))) at 2.
 apply add_cancel_l.
 Qed.
@@ -314,7 +314,7 @@ Qed.
 Theorem div_lt_upper_bound:
   forall a b q, 0<=a -> 0<b -> a < b*q -> a/b < q.
 Proof.
-intros.
+intros a b q ? ? ?.
 rewrite (mul_lt_mono_pos_l b) by order.
 apply le_lt_trans with a; auto.
 apply mul_div_le; auto.
@@ -323,7 +323,7 @@ Qed.
 Theorem div_le_upper_bound:
   forall a b q, 0<=a -> 0<b -> a <= b*q -> a/b <= q.
 Proof.
-intros.
+intros a b q ? ? ?.
 rewrite (mul_le_mono_pos_l _ _ b) by order.
 apply le_trans with a; auto.
 apply mul_div_le; auto.
@@ -362,7 +362,7 @@ Qed.
 Lemma mod_add : forall a b c, 0<=a -> 0<=a+b*c -> 0<c ->
  (a + b * c) mod c == a mod c.
 Proof.
- intros.
+ intros a b c ? ? ?.
  symmetry.
  apply mod_unique with (a/c+b); auto.
  - apply mod_bound_pos; auto.
@@ -373,7 +373,7 @@ Qed.
 Lemma div_add : forall a b c, 0<=a -> 0<=a+b*c -> 0<c ->
  (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.
@@ -393,7 +393,7 @@ Qed.
 Lemma div_mul_cancel_r : forall a b c, 0<=a -> 0<b -> 0<c ->
  (a*c)/(b*c) == a/b.
 Proof.
- intros.
+ intros a b c ? ? ?.
  symmetry.
  apply div_unique with ((a mod b)*c).
  - apply mul_nonneg_nonneg; order.
@@ -409,13 +409,13 @@ Qed.
 Lemma div_mul_cancel_l : forall a b c, 0<=a -> 0<b -> 0<c ->
  (c*a)/(c*b) == a/b.
 Proof.
- intros. rewrite !(mul_comm c); apply div_mul_cancel_r; auto.
+ intros a b c ? ? ?. rewrite !(mul_comm c); apply div_mul_cancel_r; auto.
 Qed.
 
 Lemma mul_mod_distr_l: forall a b c, 0<=a -> 0<b -> 0<c ->
   (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; auto.
@@ -427,7 +427,7 @@ Qed.
 Lemma mul_mod_distr_r: forall a b c, 0<=a -> 0<b -> 0<c ->
   (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.
 
 (** Operations modulo. *)
@@ -435,7 +435,7 @@ Qed.
 Theorem mod_mod: forall a n, 0<=a -> 0<n ->
  (a mod n) mod n == a mod n.
 Proof.
- intros. destruct (mod_bound_pos a n); auto. now rewrite mod_small_iff.
+ intros a n ? ?. destruct (mod_bound_pos a n); auto. now rewrite mod_small_iff.
 Qed.
 
 Lemma mul_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n ->
@@ -454,13 +454,14 @@ Qed.
 Lemma mul_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a*(b mod n)) mod n == (a*b) mod n.
 Proof.
- intros. rewrite !(mul_comm a). apply mul_mod_idemp_l; auto.
+ intros a b n ? ? ?. rewrite !(mul_comm a). apply mul_mod_idemp_l; auto.
 Qed.
 
 Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a * b) mod n == ((a mod n) * (b mod n)) mod n.
 Proof.
-  intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. - reflexivity.
+  intros a b n ? ? ?. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial.
+  - reflexivity.
   - now destruct (mod_bound_pos b n).
 Qed.
 
@@ -478,13 +479,14 @@ Qed.
 Lemma add_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a+(b mod n)) mod n == (a+b) mod n.
 Proof.
- intros. rewrite !(add_comm a). apply add_mod_idemp_l; auto.
+ intros a b n ? ? ?. rewrite !(add_comm a). apply add_mod_idemp_l; auto.
 Qed.
 
 Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a+b) mod n == (a mod n + b mod n) mod n.
 Proof.
-  intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. - reflexivity.
+  intros a b n ? ? ?. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial.
+  - reflexivity.
   - now destruct (mod_bound_pos b n).
 Qed.
 
@@ -525,7 +527,7 @@ Qed.
 Theorem div_mul_le:
  forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a/b) <= (c*a)/b.
 Proof.
- intros.
+ intros a b c ? ? ?.
  apply div_le_lower_bound; auto.
  - apply mul_nonneg_nonneg; auto.
  - rewrite mul_assoc, (mul_comm b c), <- mul_assoc.
@@ -538,7 +540,7 @@ Qed.
 Lemma mod_divides : forall a b, 0<=a -> 0<b ->
  (a mod b == 0 <-> exists c, a == b*c).
 Proof.
- split.
+ intros a b ? ?; split.
  - intros. exists (a/b). rewrite div_exact; auto.
  - intros (c,Hc). rewrite Hc, mul_comm. apply mod_mul; auto.
    rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order.
diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v
index 63cc725aec..c542c3fc2c 100644
--- a/theories/Numbers/NatInt/NZGcd.v
+++ b/theories/Numbers/NatInt/NZGcd.v
@@ -147,7 +147,7 @@ Qed.
 Lemma mul_divide_cancel_r : forall n m p, p ~= 0 ->
  ((n * p | m * p) <-> (n | m)).
 Proof.
- intros. rewrite 2 (mul_comm _ p). now apply mul_divide_cancel_l.
+ intros n m p ?. rewrite 2 (mul_comm _ p). now apply mul_divide_cancel_l.
 Qed.
 
 Lemma divide_add_r : forall n m p, (n | m) -> (n | p) -> (n | m + p).
@@ -215,7 +215,7 @@ Qed.
 Lemma gcd_divide_iff : forall n m p,
   (p | gcd n m) <-> (p | n) /\ (p | m).
 Proof.
-  intros. split. - split.
+  intros n m p. split. - split.
                    + transitivity (gcd n m); trivial using gcd_divide_l.
                    + transitivity (gcd n m); trivial using gcd_divide_r.
   - intros (H,H'). now apply gcd_greatest.
@@ -273,18 +273,18 @@ Qed.
 
 Lemma gcd_eq_0_l : forall n m, gcd n m == 0 -> n == 0.
 Proof.
- intros.
+ intros n m H.
  generalize (gcd_divide_l n m). rewrite H. apply divide_0_l.
 Qed.
 
 Lemma gcd_eq_0_r : forall n m, gcd n m == 0 -> m == 0.
 Proof.
- intros. apply gcd_eq_0_l with n. now rewrite gcd_comm.
+ intros n m ?. apply gcd_eq_0_l with n. now rewrite gcd_comm.
 Qed.
 
 Lemma gcd_eq_0 : forall n m, gcd n m == 0 <-> n == 0 /\ m == 0.
 Proof.
-  intros. split.
+  intros n m. split.
   - split.
     + now apply gcd_eq_0_l with m.
     + now apply gcd_eq_0_r with n.
diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v
index 5491d7ab04..526af2f9df 100644
--- a/theories/Numbers/NatInt/NZLog.v
+++ b/theories/Numbers/NatInt/NZLog.v
@@ -335,7 +335,7 @@ Qed.
 Lemma log2_succ_or : forall a,
  log2 (S a) == S (log2 a) \/ log2 (S a) == log2 a.
 Proof.
- intros.
+ intros a.
  destruct (le_gt_cases (log2 (S a)) (log2 a)) as [H|H].
  - right. generalize (log2_le_mono _ _ (le_succ_diag_r a)); order.
  - left. apply le_succ_l in H. generalize (log2_succ_le a); order.
@@ -601,7 +601,7 @@ Lemma log2_log2_up_exact :
 Proof.
  intros a Ha.
  split.
- - intros. exists (log2 a).
+ - intros H. exists (log2 a).
    generalize (log2_log2_up_spec a Ha). rewrite <-H.
    destruct 1; order.
  - intros (b,Hb). rewrite Hb.
@@ -806,8 +806,8 @@ Qed.
 Lemma log2_up_succ_or : forall a,
  log2_up (S a) == S (log2_up a) \/ log2_up (S a) == log2_up a.
 Proof.
- intros.
- destruct (le_gt_cases (log2_up (S a)) (log2_up a)).
+ intros a.
+ destruct (le_gt_cases (log2_up (S a)) (log2_up a)) as [H|H].
  - right. generalize (log2_up_le_mono _ _ (le_succ_diag_r a)); order.
  - left. apply le_succ_l in H. generalize (log2_up_succ_le a); order.
 Qed.
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index 9ddf7cb0eb..3d6465191d 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -17,7 +17,7 @@ Include NZAddProp NZ NZBase.
 
 Theorem mul_0_r : forall n, n * 0 == 0.
 Proof.
-nzinduct n; intros; now nzsimpl.
+intro n; nzinduct n; intros; now nzsimpl.
 Qed.
 
 Theorem mul_succ_r : forall n m, n * (S m) == n * m + n.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 46749504a9..c67bbe38d8 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -46,7 +46,7 @@ Qed.
 
 Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n).
 Proof.
-nzord_induct p.
+intro p; nzord_induct p.
 - order.
 - intros p Hp _ n m Hp'. apply lt_succ_l in Hp'. order.
 - intros p Hp IH n m _. apply le_succ_l in Hp.
@@ -196,7 +196,7 @@ Qed.
 
 Theorem mul_nonneg_nonneg : forall n m, 0 <= n -> 0 <= m -> 0 <= n*m.
 Proof.
-intros. rewrite <- (mul_0_l m). apply mul_le_mono_nonneg; order.
+intros n m Hn Hm. rewrite <- (mul_0_l m). apply mul_le_mono_nonneg; order.
 Qed.
 
 Theorem mul_pos_cancel_l : forall n m, 0 < n -> (0 < n*m <-> 0 < m).
@@ -343,7 +343,7 @@ Qed.
 
 Lemma square_nonneg : forall a, 0 <= a * a.
 Proof.
- intros. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0).
+ intro a. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0).
  - now apply mul_le_mono_nonpos_l.
  - apply mul_le_mono_nonneg_l; order.
 Qed.
@@ -391,7 +391,7 @@ Qed.
 Lemma quadmul_le_squareadd : forall a b, 0<=a -> 0<=b ->
  2*2*a*b <= (a+b)*(a+b).
 Proof.
- intros.
+ intros a b Ha Hb.
  nzsimpl'.
  rewrite !mul_add_distr_l, !mul_add_distr_r.
  rewrite (add_comm _ (b*b)), add_assoc.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index d576902c5c..68bb974c5d 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -65,7 +65,7 @@ Qed.
 
 Theorem le_succ_l : forall n m, S n <= m <-> n < m.
 Proof.
-intro n; nzinduct m n.
+intros n m; nzinduct m n.
 - split; intro H. + false_hyp H nle_succ_diag_l. + false_hyp H lt_irrefl.
 - intro m.
   rewrite (lt_eq_cases (S n) (S m)), !lt_succ_r, (lt_eq_cases n m), succ_inj_wd.
@@ -362,7 +362,7 @@ induction does not go through, so we need to use strong
 Lemma lt_exists_pred_strong :
   forall z n m, z < m -> m <= n -> exists k, m == S k /\ z <= k.
 Proof.
-intro z; nzinduct n z.
+intros z n; nzinduct n z.
 - order.
 - intro n; split; intros IH m H1 H2.
   + apply le_succ_r in H2. destruct H2 as [H2 | H2].
@@ -373,7 +373,7 @@ Qed.
 Theorem lt_exists_pred :
   forall z n, z < n -> exists k, n == S k /\ z <= k.
 Proof.
-intros z n H; apply lt_exists_pred_strong with (z := z) (n := n).
+intros z n H; apply (lt_exists_pred_strong z n).
 - assumption. - apply le_refl.
 Qed.
 
@@ -428,12 +428,12 @@ Qed.
 
 Lemma A'A_right : (forall n, A' n) -> forall n, z <= n -> A n.
 Proof.
-intros H1 n H2. apply H1 with (n := S n); [assumption | apply lt_succ_diag_r].
+intros H1 n H2. apply (H1 (S n)); [assumption | apply lt_succ_diag_r].
 Qed.
 
 Theorem strong_right_induction: right_step' -> forall n, z <= n -> A n.
 Proof.
-intro RS'; apply A'A_right; unfold A'; nzinduct n z;
+intro RS'; apply A'A_right; unfold A'; intro n; nzinduct n z;
 [apply rbase | apply rs'_rs''; apply RS'].
 Qed.
 
@@ -504,7 +504,7 @@ Qed.
 
 Theorem strong_left_induction: left_step' -> forall n, n <= z -> A n.
 Proof.
-intro LS'; apply A'A_left; unfold A'; nzinduct n (S z);
+intro LS'; apply A'A_left; unfold A'; intro n; nzinduct n (S z);
 [apply lbase | apply ls'_ls''; apply LS'].
 Qed.
 
@@ -629,8 +629,7 @@ Qed.
 Theorem lt_wf : well_founded Rlt.
 Proof.
 unfold well_founded.
-apply strong_right_induction' with (z := z).
-- auto with typeclass_instances.
+apply (strong_right_induction' _ _ z).
 - intros n H; constructor; intros y [H1 H2].
   apply nle_gt in H2. elim H2. now apply le_trans with z.
 - intros n H1 H2; constructor; intros m [H3 H4]. now apply H2.
@@ -639,8 +638,7 @@ Qed.
 Theorem gt_wf : well_founded Rgt.
 Proof.
 unfold well_founded.
-apply strong_left_induction' with (z := z).
-- auto with typeclass_instances.
+apply (strong_left_induction' _ _ z).
 - intros n H; constructor; intros y [H1 H2].
   apply nle_gt in H2.
   + elim H2.
diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v
index ee6f4014f0..07a33e3f67 100644
--- a/theories/Numbers/NatInt/NZParity.v
+++ b/theories/Numbers/NatInt/NZParity.v
@@ -47,7 +47,7 @@ Qed.
 
 Lemma Even_or_Odd : forall x, Even x \/ Odd x.
 Proof.
- nzinduct x.
+ intro x; nzinduct x.
  - left. exists 0. now nzsimpl.
  - intros x.
    split; intros [(y,H)|(y,H)].
@@ -86,7 +86,7 @@ Qed.
 
 Lemma orb_even_odd : forall n, orb (even n) (odd n) = true.
 Proof.
- intros.
+ intros n.
  destruct (Even_or_Odd n) as [H|H].
  - rewrite <- even_spec in H. now rewrite H.
  - rewrite <- odd_spec in H. now rewrite H, orb_true_r.
@@ -94,7 +94,7 @@ Qed.
 
 Lemma negb_odd : forall n, negb (odd n) = even n.
 Proof.
- intros.
+ intros n.
  generalize (Even_or_Odd n) (Even_Odd_False n).
  rewrite <- even_spec, <- odd_spec.
  destruct (odd n), (even n) ; simpl; intuition.
@@ -188,7 +188,7 @@ Qed.
 
 Lemma even_add : forall n m, even (n+m) = Bool.eqb (even n) (even m).
 Proof.
- intros.
+ intros n m.
  case_eq (even n); case_eq (even m);
   rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec;
   intros (m',Hm) (n',Hn).
@@ -200,7 +200,7 @@ Qed.
 
 Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m).
 Proof.
- intros. rewrite <- !negb_even. rewrite even_add.
+ intros n m. rewrite <- !negb_even. rewrite even_add.
  now destruct (even n), (even m).
 Qed.
 
@@ -208,7 +208,7 @@ Qed.
 
 Lemma even_mul : forall n m, even (mul n m) = even n || even m.
 Proof.
- intros.
+ intros n m.
  case_eq (even n); simpl; rewrite ?even_spec.
  - intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc.
  - case_eq (even m); simpl; rewrite ?even_spec.
@@ -222,7 +222,7 @@ Qed.
 
 Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m.
 Proof.
- intros. rewrite <- !negb_even. rewrite even_mul.
+ intros n m. rewrite <- !negb_even. rewrite even_mul.
  now destruct (even n), (even m).
 Qed.
 
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
index 01a15686e0..3b2a496229 100644
--- a/theories/Numbers/NatInt/NZPow.v
+++ b/theories/Numbers/NatInt/NZPow.v
@@ -238,7 +238,7 @@ Qed.
 Lemma pow_le_mono : forall a b c d, 0<a<=c -> b<=d ->
  a^b <= c^d.
 Proof.
- intros. transitivity (a^d).
+ intros a b c d ? ?. transitivity (a^d).
  - apply pow_le_mono_r; intuition order.
  - apply pow_le_mono_l; intuition order.
 Qed.
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index 446ed07b53..4122632603 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -58,7 +58,7 @@ Qed.
 
 Lemma sqrt_nonneg : forall a, 0<=√a.
 Proof.
- intros. destruct (lt_ge_cases a 0) as [Ha|Ha].
+ intros a. destruct (lt_ge_cases a 0) as [Ha|Ha].
  - now rewrite (sqrt_neg _ Ha).
  - apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order.
 Qed.
@@ -429,7 +429,7 @@ Qed.
 
 Lemma sqrt_up_nonneg : forall a, 0<=√°a.
 Proof.
- intros. destruct (le_gt_cases a 0) as [Ha|Ha].
+ intros a. destruct (le_gt_cases a 0) as [Ha|Ha].
  - now rewrite sqrt_up_eqn0.
  - rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg.
 Qed.
@@ -527,7 +527,7 @@ Lemma sqrt_sqrt_up_exact :
  forall a, 0<=a -> (√a == √°a <-> exists b, 0<=b /\ a == b²).
 Proof.
  intros a Ha.
- split. - intros. exists √a.
+ split. - intros H. exists √a.
           split. + apply sqrt_nonneg.
           + generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order.
  - intros (b & Hb & Hb'). rewrite Hb'.
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 72183f76e6..51be2bd956 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -54,8 +54,7 @@ Section Properties.
     Lemma clos_rt_idempotent : inclusion (R*)* R*.
     Proof.
       red.
-      induction 1; auto with sets.
-      intros.
+      induction 1 as [x y H|x|x y z H IH H0 IH0]; auto with sets.
       apply rt_trans with y; auto with sets.
     Qed.
 
@@ -70,7 +69,7 @@ Section Properties.
       inclusion (clos_refl_trans R) (clos_refl_sym_trans R).
     Proof.
       red.
-      induction 1; auto with sets.
+      induction 1 as [x y H|x|x y z H IH H0 IH0]; auto with sets.
       apply rst_trans with y; auto with sets.
     Qed.
 
@@ -90,7 +89,7 @@ Section Properties.
       clos_trans R x z.
     Proof.
       induction 1 as [b d H1|b|a b d H1 H2 IH1 IH2]; auto.
-      intro H. apply t_trans with (y:=d); auto.
+      intro H. apply (t_trans _ _ _ d); auto.
       constructor. auto.
     Qed.
 
@@ -111,7 +110,7 @@ Section Properties.
       (clos_refl_sym_trans R).
     Proof.
       red.
-      induction 1; auto with sets.
+      induction 1 as [x y H|x|x y H IH|x y z H IH H0 IH0]; auto with sets.
       apply rst_trans with y; auto with sets.
     Qed.
 
@@ -128,7 +127,7 @@ Section Properties.
 
     Lemma clos_t1n_trans : forall x y, clos_trans_1n R x y -> clos_trans R x y.
     Proof.
-     induction 1.
+     induction 1 as [x y H|x y z H H0 IH0].
      - left; assumption.
      - right with y; auto.
        left; auto.
@@ -136,9 +135,10 @@ Section Properties.
 
     Lemma clos_trans_t1n : forall x y, clos_trans R x y -> clos_trans_1n R x y.
     Proof.
-      induction 1.
+      induction 1 as [x y H|x y z H IHclos_trans1 H0 IHclos_trans2].
       - left; assumption.
-      - generalize IHclos_trans2; clear IHclos_trans2; induction IHclos_trans1.
+      - generalize IHclos_trans2; clear IHclos_trans2.
+        induction IHclos_trans1 as [x y H1|x y z0 H1 ? IHIHclos_trans1].
         + right with y; auto.
         + right with y; auto.
       eapply IHIHclos_trans1; auto.
@@ -157,7 +157,7 @@ Section Properties.
 
     Lemma clos_tn1_trans : forall x y, clos_trans_n1 R x y -> clos_trans R x y.
     Proof.
-      induction 1.
+      induction 1 as [y H|y z H H0 ?].
       - left; assumption.
       - right with y; auto.
         left; assumption.
@@ -165,13 +165,13 @@ Section Properties.
 
     Lemma clos_trans_tn1 :  forall x y, clos_trans R x y -> clos_trans_n1 R x y.
     Proof.
-      induction 1.
+      induction 1 as [x y H|x y z H IHclos_trans1 H0 IHclos_trans2].
       - left; assumption.
       - elim IHclos_trans2.
         + intro y0; right with y.
           *  auto.
           * auto.
-        + intros.
+        + intro y0; intros.
           right with y0; auto.
     Qed.
 
@@ -201,7 +201,7 @@ Section Properties.
     Lemma clos_rt1n_rt : forall x y,
         clos_refl_trans_1n R x y -> clos_refl_trans R x y.
     Proof.
-      induction 1.
+      induction 1 as [|x y z].
       - constructor 2.
       - constructor 3 with y; auto.
         constructor 1; auto.
@@ -210,14 +210,14 @@ Section Properties.
     Lemma clos_rt_rt1n : forall x y,
         clos_refl_trans R x y -> clos_refl_trans_1n R x y.
     Proof.
-      induction 1.
+      induction 1 as [| |x y z H IHclos_refl_trans1 H0 IHclos_refl_trans2].
       - apply clos_rt1n_step; assumption.
       - left.
       - generalize IHclos_refl_trans2; clear IHclos_refl_trans2;
-          induction IHclos_refl_trans1; auto.
+          induction IHclos_refl_trans1 as [|x y z0 H1 ? IH]; auto.
 
         right with y; auto.
-        eapply IHIHclos_refl_trans1; auto.
+        eapply IH; auto.
         apply clos_rt1n_rt; auto.
     Qed.
 
@@ -235,7 +235,7 @@ Section Properties.
     Lemma clos_rtn1_rt : forall x y,
         clos_refl_trans_n1 R x y -> clos_refl_trans R x y.
     Proof.
-      induction 1.
+      induction 1 as [|y z].
       - constructor 2.
       - constructor 3 with y; auto.
         constructor 1; assumption.
@@ -244,11 +244,11 @@ Section Properties.
     Lemma clos_rt_rtn1 :  forall x y,
         clos_refl_trans R x y -> clos_refl_trans_n1 R x y.
     Proof.
-      induction 1.
+      induction 1 as [| |x y z H1 IH1 H2 IH2].
       - apply clos_rtn1_step; auto.
       - left.
-      - elim IHclos_refl_trans2; auto.
-        intros.
+      - elim IH2; auto.
+        intro y0; intros.
         right with y0; auto.
     Qed.
 
@@ -267,16 +267,16 @@ Section Properties.
 	(forall y z:A, clos_refl_trans R x y -> P y -> R y z -> P z) ->
 	forall z:A, clos_refl_trans R x z -> P z.
     Proof.
-      intros.
+      intros x P H H0 z H1.
       revert H H0.
-      induction H1; intros; auto with sets.
-      - apply H1 with x; auto with sets.
+      induction H1 as [x| |x y z H1 IH1 H2 IH2]; intros HP HIS; auto with sets.
+      - apply HIS with x; auto with sets.
 
-      - apply IHclos_refl_trans2.
-        + apply IHclos_refl_trans1; auto with sets.
+      - apply IH2.
+        + apply IH1; auto with sets.
 
-        + intros.
-          apply H0 with y0; auto with sets.
+        + intro y0; intros;
+          apply HIS with y0; auto with sets.
           apply rt_trans with y; auto with sets.
     Qed.
 
@@ -286,7 +286,7 @@ Section Properties.
       P z ->
       (forall x y, R x y -> clos_refl_trans_1n R y z -> P y -> P x) ->
       forall x, clos_refl_trans_1n R x z -> P x.
-      induction 3; auto.
+      intros P z H H0 x; induction 1 as [|x y z]; auto.
       apply H0 with y; auto.
     Qed.
 
@@ -309,7 +309,7 @@ Section Properties.
     Lemma clos_rst1n_rst  : forall x y,
       clos_refl_sym_trans_1n R x y -> clos_refl_sym_trans R x y.
     Proof.
-      induction 1.
+      induction 1 as [|x y z H].
       - constructor 2.
       - constructor 4 with y; auto.
         case H;[constructor 1|constructor 3; constructor 1]; auto.
@@ -317,7 +317,7 @@ Section Properties.
 
     Lemma clos_rst1n_trans : forall x y z, clos_refl_sym_trans_1n R x y ->
         clos_refl_sym_trans_1n R y z -> clos_refl_sym_trans_1n R x z.
-      induction 1.
+      induction 1 as [|x y z0].
       - auto.
       - intros; right with y; eauto.
     Qed.
@@ -335,7 +335,7 @@ Section Properties.
 
     Lemma clos_rst_rst1n  : forall x y,
       clos_refl_sym_trans R x y -> clos_refl_sym_trans_1n R x y.
-      induction 1.
+      induction 1 as [x y| | |].
       - constructor 2 with y; auto.
         constructor 1.
       - constructor 1.
@@ -357,7 +357,7 @@ Section Properties.
     Lemma clos_rstn1_rst : forall x y,
       clos_refl_sym_trans_n1 R x y -> clos_refl_sym_trans R x y.
     Proof.
-      induction 1.
+      induction 1 as [|y z H].
       - constructor 2.
       - constructor 4 with y; auto.
         case H;[constructor 1|constructor 3; constructor 1]; auto.
@@ -367,10 +367,9 @@ Section Properties.
       clos_refl_sym_trans_n1 R y z -> clos_refl_sym_trans_n1 R x z.
     Proof.
       intros x y z H1 H2.
-      induction H2.
+      induction H2 as [|y0 z].
       - auto.
-      - intros.
-        right with y0; eauto.
+      - right with y0; eauto.
     Qed.
 
     Lemma clos_rstn1_sym : forall x y, clos_refl_sym_trans_n1 R x y ->
@@ -387,7 +386,7 @@ Section Properties.
     Lemma clos_rst_rstn1 : forall x y,
       clos_refl_sym_trans R x y -> clos_refl_sym_trans_n1 R x y.
     Proof.
-      induction 1.
+      induction 1 as [x| | |].
       - constructor 2 with x; auto.
         constructor 1.
       - constructor 1.
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index 0a5128f093..dea76694f3 100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -16,16 +16,16 @@ Lemma inverse_image_of_equivalence :
   forall (A B:Type) (f:A -> B) (r:relation B),
     equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
 Proof.
-  intros; split; elim H; red; auto.
+  intros A B f r H; split; elim H; red; auto.
   intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
 Qed.
 
 Lemma inverse_image_of_eq :
   forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y).
 Proof.
-  split; red;
+  intros A B f; split; red;
     [  (* reflexivity *) reflexivity
-      |  (* transitivity *) intros; transitivity (f y); assumption
+      |  (* transitivity *) intros x y z; transitivity (f y); assumption
       |  (* symmetry *) intros; symmetry ; assumption ].
 Qed.
 
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index b10c4f3768..cec1033fdf 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -33,7 +33,7 @@ Defined.
 
 Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z.
 Proof.
-  unfold Setoid_Theory in s. intros ; transitivity y ; assumption.
+  unfold Setoid_Theory in s. intros x y z H0 H1 ; transitivity y ; assumption.
 Defined.
 
 (** Some tactics for manipulating Setoid Theory not officially
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 8d20ce77f9..1af6aebec6 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -629,9 +629,9 @@ Module TOMaxEqDec_to_Compare
   if eq_dec x y then Eq
   else if eq_dec (M.max x y) y then Lt else Gt.
 
- Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+ Lemma compare_spec x y : CompSpec eq lt x y (compare x y).
  Proof.
- intros; unfold compare; repeat destruct eq_dec; auto; constructor.
+ unfold compare; repeat destruct eq_dec; auto; constructor.
  - destruct (lt_total x y); auto.
    absurd (x==y); auto. transitivity (max x y); auto.
    symmetry. apply max_l. rewrite le_lteq; intuition.
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index 94938c1d4d..b3e3b6e853 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -165,7 +165,7 @@ End OT_to_Full.
 
 Module OTF_LtIsTotal (Import O:OrderedTypeFull') <: LtIsTotal O.
  Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
- Proof. intros; destruct (compare_spec x y); auto. Qed.
+ Proof. intros x y; destruct (compare_spec x y); auto. Qed.
 End OTF_LtIsTotal.
 
 Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
@@ -250,7 +250,7 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool.
 
  Lemma leb_le : forall x y, leb x y <-> x <= y.
  Proof.
- intros. unfold leb. rewrite le_lteq.
+ intros x y. unfold leb. rewrite le_lteq.
  destruct (compare_spec x y) as [EQ|LT|GT]; split; auto.
  - discriminate.
  - intros LE. elim (StrictOrder_Irreflexive x).
@@ -261,7 +261,7 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool.
 
  Lemma leb_total : forall x y, leb x y \/ leb y x.
  Proof.
- intros. rewrite 2 leb_le. rewrite 2 le_lteq.
+ intros x y. rewrite 2 leb_le. rewrite 2 le_lteq.
  destruct (compare_spec x y); intuition.
  Qed.
 
@@ -302,7 +302,7 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull.
 
  Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
  Proof.
- intros. unfold compare.
+ intros x y. unfold compare.
  case_eq (x <=? y).
  - case_eq (y <=? x).
    + constructor. split; auto.
@@ -352,7 +352,7 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull.
 
  Definition le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
  Proof.
- intros.
+ intros x y.
  unfold lt, eq, le.
  split; [ | intuition ].
  intros LE.
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index d5a76ee69f..4ac54d280a 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -102,10 +102,10 @@ Module OrderedTypeFullFacts (Import O:OrderedTypeFull').
  Proof. iorder. Qed.
 
  Lemma le_or_gt : forall x y, x<=y \/ y<x.
- Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed.
+ Proof. intros x y. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed.
 
  Lemma lt_or_ge : forall x y, x<y \/ y<=x.
- Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed.
+ Proof. intros x y. rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed.
 
  Lemma eq_is_le_ge : forall x y, x==y <-> x<=y /\ y<=x.
  Proof. iorder. Qed.
@@ -175,11 +175,11 @@ Module OrderedTypeFacts (Import O: OrderedType').
 
   Definition eqb x y : bool := if eq_dec x y then true else false.
 
-  Lemma if_eq_dec : forall x y (B:Type)(b b':B),
+  Lemma if_eq_dec x y (B:Type)(b b':B) :
     (if eq_dec x y then b else b') =
     (match compare x y with Eq => b | _ => b' end).
   Proof.
-  intros; destruct eq_dec; elim_compare x y; auto; order.
+  destruct eq_dec; elim_compare x y; auto; order.
   Qed.
 
   Lemma eqb_alt :
@@ -257,7 +257,7 @@ Definition compare := flip O.compare.
 
 Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
 Proof.
-intros; unfold compare, eq, lt, flip.
+intros x y; unfold compare, eq, lt, flip.
 destruct (O.compare_spec y x); auto with relations.
 Qed.
 
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v
index 408348139d..1c8073972d 100644
--- a/theories/Structures/OrdersTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -100,9 +100,9 @@ Definition interp_ord o :=
  match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end.
 Local Notation "#" := interp_ord.
 
-Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
+Lemma trans o o' x y z : #o x y -> #o' y z -> #(o+o') x z.
 Proof.
-destruct o, o'; simpl; intros x y z;
+destruct o, o'; simpl;
 rewrite ?P.le_lteq; intuition auto;
 subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
 Qed.