Merge PR #13730: Lint stdlib with -mangle-names #6

Reviewed-by: anton-trunov

9 files changed, 183 insertions, 155 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 6978fa1ddf..a1a4da6f37 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -87,7 +87,7 @@ Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left.
 
   Next Obligation.
   Proof.
-    destruct x ; destruct y.
+    do 2 match goal with [ x : () |- _ ] => destruct x end.
     reflexivity.
   Qed.
 
@@ -142,7 +142,10 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq :=
       | _, _ => in_right
     end }.
 
-  Next Obligation. destruct y ; unfold not in *; eauto. Defined.
+  Next Obligation.
+    match goal with y : list _ |- _ => destruct y end ;
+    unfold not in *; eauto.
+  Defined.
 
   Solve Obligations with unfold equiv, complement in * ; 
     program_simpl ; intuition (discriminate || eauto).
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 6a98af39aa..3e71a60fa6 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -87,7 +87,7 @@ Tactic Notation "clsubst" "*" := clsubst_nofail.
 
 Lemma nequiv_equiv_trans : forall `{Setoid A} (x y z : A), x =/= y -> y == z -> x =/= z.
 Proof with auto.
-  intros; intro.
+  intros A ? x y z H H0 H1.
   assert(z == y) by (symmetry ; auto).
   assert(x == y) by (transitivity z ; eauto).
   contradiction.
@@ -95,7 +95,7 @@ Qed.
 
 Lemma equiv_nequiv_trans : forall `{Setoid A} (x y z : A), x == y -> y =/= z -> x =/= z.
 Proof.
-  intros; intro.
+  intros A ? x y z **; intro.
   assert(y == x) by (symmetry ; auto).
   assert(y == z) by (transitivity x ; eauto).
   contradiction.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 2947c4831f..f4220e3aa1 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -96,7 +96,7 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
 
   Next Obligation.
   Proof.
-    destruct x ; destruct y.
+    do 2 match goal with x : () |- _ => destruct x end.
     reflexivity.
   Qed.
 
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 826815410a..69b158a87e 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -71,7 +71,7 @@ Hint Constructors NoDupA : core.
 Lemma NoDupA_altdef : forall l,
  NoDupA l <-> ForallOrdPairs (complement eqA) l.
 Proof.
- split; induction 1; constructor; auto.
+ split; induction 1 as [|a l H rest]; constructor; auto.
  rewrite Forall_forall. intros b Hb.
  intro Eq; elim H. rewrite InA_alt. exists b; auto.
  rewrite InA_alt; intros (a' & Haa' & Ha').
@@ -85,7 +85,7 @@ Definition inclA l l' := forall x, InA x l -> InA x l'.
 Definition equivlistA l l' := forall x, InA x l <-> InA x l'.
 
 Lemma incl_nil l : inclA nil l.
-Proof. intro. intros. inversion H. Qed.
+Proof. intros a H. inversion H. Qed.
 #[local]
 Hint Resolve incl_nil : list.
 
@@ -128,7 +128,7 @@ Qed.
 Global Instance eqlistA_equiv : Equivalence eqlistA.
 Proof.
  constructor; red.
- induction x; auto.
+ intros x; induction x; auto.
  induction 1; auto.
  intros x y z H; revert z; induction H; auto.
  inversion 1; subst; auto. invlist eqlistA; eauto with *.
@@ -138,9 +138,9 @@ Qed.
 
 Global Instance eqlistA_equivlistA : subrelation eqlistA equivlistA.
 Proof.
-  intros x x' H. induction H.
+  intros x x' H. induction H as [|? ? ? ? H ? IHeqlistA].
   intuition.
-  red; intros.
+  red; intros x0.
   rewrite 2 InA_cons.
   rewrite (IHeqlistA x0), H; intuition.
 Qed.
@@ -165,7 +165,7 @@ Hint Immediate InA_eqA : core.
 
 Lemma In_InA : forall l x, In x l -> InA x l.
 Proof.
- simple induction l; simpl; intuition.
+ intros l; induction l; simpl; intuition.
  subst; auto.
 Qed.
 #[local]
@@ -174,8 +174,9 @@ Hint Resolve In_InA : core.
 Lemma InA_split : forall l x, InA x l ->
  exists l1 y l2, eqA x y /\ l = l1++y::l2.
 Proof.
-induction l; intros; inv.
+intros l; induction l as [|a l IHl]; intros x H; inv.
 exists (@nil A); exists a; exists l; auto.
+match goal with H' : InA x l |- _ => rename H' into H0 end.
 destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))).
 exists (a::l1); exists y; exists l2; auto.
 split; simpl; f_equal; auto.
@@ -184,9 +185,10 @@ Qed.
 Lemma InA_app : forall l1 l2 x,
  InA x (l1 ++ l2) -> InA x l1 \/ InA x l2.
 Proof.
- induction l1; simpl in *; intuition.
+ intros l1; induction l1 as [|a l1 IHl1]; simpl in *; intuition.
  inv; auto.
- elim (IHl1 l2 x H0); auto.
+ match goal with H0' : InA _ (l1 ++ _) |- _ => rename H0' into H0 end.
+ elim (IHl1 _ _ H0); auto.
 Qed.
 
 Lemma InA_app_iff : forall l1 l2 x,
@@ -194,7 +196,7 @@ Lemma InA_app_iff : forall l1 l2 x,
 Proof.
  split.
  apply InA_app.
- destruct 1; generalize H; do 2 rewrite InA_alt.
+ destruct 1 as [H|H]; generalize H; do 2 rewrite InA_alt.
  destruct 1 as (y,(H1,H2)); exists y; split; auto.
  apply in_or_app; auto.
  destruct 1 as (y,(H1,H2)); exists y; split; auto.
@@ -240,11 +242,12 @@ Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' ->
   (forall x, InA x l -> InA x l' -> False) ->
   NoDupA (l++l').
 Proof.
-induction l; simpl; auto; intros.
+intros l; induction l as [|a l IHl]; simpl; auto; intros l' H H0 H1.
 inv.
 constructor.
 rewrite InA_alt; intros (y,(H4,H5)).
 destruct (in_app_or _ _ _ H5).
+match goal with H2' : ~ InA a l |- _ => rename H2' into H2 end.
 elim H2.
 rewrite InA_alt.
 exists y; auto.
@@ -253,13 +256,13 @@ auto.
 rewrite InA_alt.
 exists y; auto.
 apply IHl; auto.
-intros.
+intros x ? ?.
 apply (H1 x); auto.
 Qed.
 
 Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l).
 Proof.
-induction l.
+intros l; induction l.
 simpl; auto.
 simpl; intros.
 inv.
@@ -270,17 +273,17 @@ intros x.
 rewrite InA_alt.
 intros (x1,(H2,H3)).
 intro; inv.
-destruct H0.
-rewrite <- H4, H2.
+match goal with H0 : ~ InA _ _ |- _ => destruct H0 end.
+match goal with H4 : eqA x ?x' |- InA ?x' _ => rewrite <- H4, H2 end.
 apply In_InA.
 rewrite In_rev; auto.
 Qed.
 
 Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l').
 Proof.
- induction l; simpl in *; intros; inv; auto.
+ intros l; induction l; simpl in *; intros; inv; auto.
  constructor; eauto.
- contradict H0.
+ match goal with H0 : ~ InA _ _ |- _ => contradict H0 end.
  rewrite InA_app_iff in *.
  rewrite InA_cons.
  intuition.
@@ -288,17 +291,17 @@ Qed.
 
 Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l').
 Proof.
- induction l; simpl in *; intros; inv; auto.
+ intros l; induction l as [|a l IHl]; simpl in *; intros l' x H; inv; auto.
  constructor; eauto.
- assert (H2:=IHl _ _ H1).
+ match goal with H1 : NoDupA (l ++ x :: l') |- _ => assert (H2:=IHl _ _ H1) end.
  inv.
  rewrite InA_cons.
  red; destruct 1.
- apply H0.
+ match goal with H0 : ~ InA a (l ++ x :: l') |- _ => apply H0 end.
  rewrite InA_app_iff in *; rewrite InA_cons; auto.
- apply H; auto.
+ auto.
  constructor.
- contradict H0.
+ match goal with H0 : ~ InA a (l ++ x :: l') |- _ => contradict H0 end.
  rewrite InA_app_iff in *; rewrite InA_cons; intuition.
  eapply NoDupA_split; eauto.
 Qed.
@@ -356,19 +359,21 @@ Lemma equivlistA_NoDupA_split l l1 l2 x y : eqA x y ->
  NoDupA (x::l) -> NoDupA (l1++y::l2) ->
  equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
 Proof.
- intros; intro a.
+ intros H H0 H1 H2; intro a.
  generalize (H2 a).
  rewrite !InA_app_iff, !InA_cons.
  inv.
  assert (SW:=NoDupA_swap H1). inv.
- rewrite InA_app_iff in H0.
+ rewrite InA_app_iff in *.
  split; intros.
- assert (~eqA a x) by (contradict H3; rewrite <- H3; auto).
+ match goal with H3 : ~ InA x l |- _ =>
+   assert (~eqA a x) by (contradict H3; rewrite <- H3; auto)
+ end.
  assert (~eqA a y) by (rewrite <- H; auto).
  tauto.
- assert (OR : eqA a x \/ InA a l) by intuition. clear H6.
+ assert (OR : eqA a x \/ InA a l) by intuition.
  destruct OR as [EQN|INA]; auto.
- elim H0.
+ match goal with H0 : ~ (InA y l1 \/ InA y l2) |- _ => elim H0 end.
  rewrite <-H,<-EQN; auto.
 Qed.
 
@@ -448,7 +453,7 @@ Qed.
 Lemma ForallOrdPairs_inclA : forall l l',
  NoDupA l' -> inclA l' l -> ForallOrdPairs R l -> ForallOrdPairs R l'.
 Proof.
-induction l' as [|x l' IH].
+intros l l'. induction l' as [|x l' IH].
 constructor.
 intros ND Incl FOP. apply FOP_cons; inv; unfold inclA in *; auto.
 rewrite Forall_forall; intros y Hy.
@@ -476,7 +481,7 @@ Lemma fold_right_commutes_restr :
   forall s1 s2 x, ForallOrdPairs R (s1++x::s2) ->
   eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
 Proof.
-induction s1; simpl; auto; intros.
+intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x H.
 reflexivity.
 transitivity (f a (f x (fold_right f i (s1++s2)))).
 apply Comp; auto.
@@ -484,7 +489,9 @@ apply IHs1.
 invlist ForallOrdPairs; auto.
 apply TraR.
 invlist ForallOrdPairs; auto.
-rewrite Forall_forall in H0; apply H0.
+match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- R a x =>
+  rewrite Forall_forall in H0; apply H0
+end.
 apply in_or_app; simpl; auto.
 Qed.
 
@@ -492,14 +499,14 @@ Lemma fold_right_equivlistA_restr :
   forall s s', NoDupA s -> NoDupA s' -> ForallOrdPairs R s ->
   equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
 Proof.
- simple induction s.
- destruct s'; simpl.
+ intros s; induction s as [|x l Hrec].
+ intros s'; destruct s' as [|a s']; simpl.
  intros; reflexivity.
- unfold equivlistA; intros.
+ unfold equivlistA; intros H H0 H1 H2.
  destruct (H2 a).
  assert (InA a nil) by auto; inv.
- intros x l Hrec s' N N' F E; simpl in *.
- assert (InA x s') by (rewrite <- (E x); auto).
+ intros s' N N' F E; simpl in *.
+ assert (InA x s') as H by (rewrite <- (E x); auto).
  destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))).
  subst s'.
  transitivity (f x (fold_right f i (s1++s2))).
@@ -520,7 +527,7 @@ Lemma fold_right_add_restr :
   forall s' s x, NoDupA s -> NoDupA s' -> ForallOrdPairs R s' -> ~ InA x s ->
   equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
 Proof.
- intros; apply (@fold_right_equivlistA_restr s' (x::s)); auto.
+ intros s' s x **; apply (@fold_right_equivlistA_restr s' (x::s)); auto.
 Qed.
 
 End Fold_With_Restriction.
@@ -532,7 +539,7 @@ Variable Tra :transpose f.
 Lemma fold_right_commutes : forall s1 s2 x,
   eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
 Proof.
-induction s1; simpl; auto; intros.
+intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x.
 reflexivity.
 transitivity (f a (f x (fold_right f i (s1++s2)))); auto.
 apply Comp; auto.
@@ -542,7 +549,7 @@ Lemma fold_right_equivlistA :
   forall s s', NoDupA s -> NoDupA s' ->
   equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
 Proof.
-intros; apply fold_right_equivlistA_restr with (R:=fun _ _ => True);
+intros; apply (fold_right_equivlistA_restr (R:=fun _ _ => True));
  repeat red; auto.
 apply ForallPairs_ForallOrdPairs; try red; auto.
 Qed.
@@ -551,7 +558,7 @@ Lemma fold_right_add :
   forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s ->
   equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
 Proof.
- intros; apply (@fold_right_equivlistA s' (x::s)); auto.
+ intros s' s x **; apply (@fold_right_equivlistA s' (x::s)); auto.
 Qed.
 
 End Fold.
@@ -571,7 +578,7 @@ Lemma fold_right_eqlistA2 :
   eqB (fold_right f i s) (fold_right f j s').
 Proof.
   intros s.
-  induction s;intros.
+  induction s as [|a s IHs];intros s' i j heqij heqss'.
   - inversion heqss'.
     subst.
     simpl.
@@ -604,7 +611,7 @@ Lemma fold_right_commutes_restr2 :
   forall s1 s2 x (i j:B) (heqij: eqB i j), ForallOrdPairs R (s1++x::s2) ->
   eqB (fold_right f i (s1++x::s2)) (f x (fold_right f j (s1++s2))).
 Proof.
-induction s1; simpl; auto; intros.
+intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x i j heqij ?.
 - apply Comp.
   + destruct eqA_equiv. apply Equivalence_Reflexive.
   + eapply fold_right_eqlistA2.
@@ -617,7 +624,9 @@ induction s1; simpl; auto; intros.
   invlist ForallOrdPairs; auto.
   apply TraR.
   invlist ForallOrdPairs; auto.
-  rewrite Forall_forall in H0; apply H0.
+  match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- _ =>
+    rewrite Forall_forall in H0; apply H0
+  end.
   apply in_or_app; simpl; auto.
   reflexivity.
 Qed.
@@ -628,14 +637,14 @@ Lemma fold_right_equivlistA_restr2 :
     equivlistA s s' -> eqB i j ->
     eqB (fold_right f i s) (fold_right f j s').
 Proof.
- simple induction s.
- destruct s'; simpl.
+ intros s; induction s as [|x l Hrec].
+ intros s'; destruct s' as [|a s']; simpl.
  intros. assumption.
- unfold equivlistA; intros.
+ unfold equivlistA; intros ? ? H H0 H1 H2 **.
  destruct (H2 a).
  assert (InA a nil) by auto; inv.
- intros x l Hrec s' i j N N' F E eqij; simpl in *.
- assert (InA x s') by (rewrite <- (E x); auto).
+ intros s' i j N N' F E eqij; simpl in *.
+ assert (InA x s') as H by (rewrite <- (E x); auto).
  destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))).
  subst s'.
  transitivity (f x (fold_right f j (s1++s2))).
@@ -663,7 +672,7 @@ Lemma fold_right_add_restr2 :
   forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ForallOrdPairs R s' -> ~ InA x s ->
   equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)).
 Proof.
- intros; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto.
+ intros s' s i j x **; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto.
 Qed.
 
 End Fold2_With_Restriction.
@@ -674,7 +683,7 @@ Lemma fold_right_commutes2 : forall s1 s2 i x x',
   eqA x x' -> 
   eqB (fold_right f i (s1++x::s2)) (f x' (fold_right f i (s1++s2))).
 Proof.
-  induction s1;simpl;intros.
+  intros s1; induction s1 as [|a s1 IHs1];simpl;intros s2 i x x' H.
 - apply Comp;auto.
   reflexivity.
 - transitivity (f a (f x' (fold_right f i (s1++s2)))); auto.
@@ -688,7 +697,7 @@ Lemma fold_right_equivlistA2 :
   equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s').
 Proof.
 red in Tra.
-intros; apply fold_right_equivlistA_restr2 with (R:=fun _ _ => True);
+intros; apply (fold_right_equivlistA_restr2 (R:=fun _ _ => True));
 repeat red; auto.
 apply ForallPairs_ForallOrdPairs; try red; auto.
 Qed.
@@ -697,9 +706,9 @@ Lemma fold_right_add2 :
   forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ~ InA x s ->
   equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)).
 Proof.
- intros.
+ intros s' s i j x **.
  replace (f x (fold_right f j s)) with (fold_right f j (x::s)) by auto.
- eapply fold_right_equivlistA2;auto. 
+ eapply fold_right_equivlistA2;auto.
 Qed.
 
 End Fold2.
@@ -710,7 +719,7 @@ Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
 
 Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }.
 Proof.
-induction l.
+intros x l; induction l as [|a l IHl].
 right; auto.
 intro; inv.
 destruct (eqA_dec x a).
@@ -729,28 +738,30 @@ Fixpoint removeA (x : A) (l : list A) : list A :=
 Lemma removeA_filter : forall x l,
   removeA x l = filter (fun y => if eqA_dec x y then false else true) l.
 Proof.
-induction l; simpl; auto.
+intros x l; induction l as [|a l IHl]; simpl; auto.
 destruct (eqA_dec x a); auto.
 rewrite IHl; auto.
 Qed.
 
 Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y.
 Proof.
-induction l; simpl; auto.
-split.
+intros l; induction l as [|a l IHl]; simpl; auto.
+intros x y; split.
 intro; inv.
 destruct 1; inv.
-intros.
+intros x y.
 destruct (eqA_dec x a) as [Heq|Hnot]; simpl; auto.
 rewrite IHl; split; destruct 1; split; auto.
 inv; auto.
-destruct H0; transitivity a; auto.
+match goal with H0 : ~ eqA x y |- _ => destruct H0 end; transitivity a; auto.
 split.
 intro; inv.
 split; auto.
 contradict Hnot.
 transitivity y; auto.
-rewrite (IHl x y) in H0; destruct H0; auto.
+match goal with H0 : InA y (removeA x l) |- _ =>
+  rewrite (IHl x y) in H0; destruct H0; auto
+end.
 destruct 1; inv; auto.
 right; rewrite IHl; auto.
 Qed.
@@ -758,7 +769,7 @@ Qed.
 Lemma removeA_NoDupA :
   forall s x, NoDupA s ->  NoDupA (removeA x s).
 Proof.
-simple induction s; simpl; intros.
+intros s; induction s as [|a s IHs]; simpl; intros x ?.
 auto.
 inv.
 destruct (eqA_dec x a); simpl; auto.
@@ -770,16 +781,16 @@ Qed.
 Lemma removeA_equivlistA : forall l l' x,
   ~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l').
 Proof.
-unfold equivlistA; intros.
+unfold equivlistA; intros l l' x H H0 x0.
 rewrite removeA_InA.
-split; intros.
+split; intros H1.
 rewrite <- H0; split; auto.
 contradict H.
 apply InA_eqA with x0; auto.
 rewrite <- (H0 x0) in H1.
 destruct H1.
 inv; auto.
-elim H2; auto.
+match goal with H2 : ~ eqA x x0 |- _ => elim H2; auto end.
 Qed.
 
 End Remove.
@@ -806,7 +817,7 @@ Hint Constructors lelistA sort : core.
 Lemma InfA_ltA :
  forall l x y, ltA x y -> InfA y l -> InfA x l.
 Proof.
- destruct l; constructor. inv; eauto.
+ intros l; destruct l; constructor. inv; eauto.
 Qed.
 
 Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA.
@@ -815,8 +826,8 @@ Proof using eqA_equiv ltA_compat. (* and not ltA_strorder *)
  inversion_clear Hll'.
  intuition.
  split; intro; inv; constructor.
- rewrite <- Hxx', <- H; auto.
- rewrite Hxx', H; auto.
+ match goal with H : eqA _ _ |- _ => rewrite <- Hxx', <- H; auto end.
+ match goal with H : eqA _ _ |- _ => rewrite Hxx', H; auto end.
 Qed.
 
 (** For compatibility, can be deduced from [InfA_compat] *)
@@ -830,9 +841,9 @@ Hint Immediate InfA_ltA InfA_eqA : core.
 Lemma SortA_InfA_InA :
  forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
 Proof.
- simple induction l.
- intros. inv.
- intros. inv.
+ intros l; induction l as [|a l IHl].
+ intros x a **. inv.
+ intros x a0 **. inv.
  setoid_replace x with a; auto.
  eauto.
 Qed.
@@ -840,13 +851,13 @@ Qed.
 Lemma In_InfA :
  forall l x, (forall y, In y l -> ltA x y) -> InfA x l.
 Proof.
- simple induction l; simpl; intros; constructor; auto.
+ intros l; induction l; simpl; intros; constructor; auto.
 Qed.
 
 Lemma InA_InfA :
  forall l x, (forall y, InA y l -> ltA x y) -> InfA x l.
 Proof.
- simple induction l; simpl; intros; constructor; auto.
+ intros l; induction l; simpl; intros; constructor; auto.
 Qed.
 
 (* In fact, this may be used as an alternative definition for InfA: *)
@@ -861,7 +872,7 @@ Qed.
 
 Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
 Proof.
- induction l1; simpl; auto.
+ intros l1; induction l1; simpl; auto.
  intros; inv; auto.
 Qed.
 
@@ -870,7 +881,7 @@ Lemma SortA_app :
  (forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
  SortA (l1 ++ l2).
 Proof.
- induction l1; simpl in *; intuition.
+ intros l1; induction l1; intros l2; simpl in *; intuition.
  inv.
  constructor; auto.
  apply InfA_app; auto.
@@ -879,8 +890,8 @@ Qed.
 
 Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
 Proof.
- simple induction l; auto.
- intros x l' H H0.
+ intros l; induction l as [|x l' H]; auto.
+ intros H0.
  inv.
  constructor; auto.
  intro.
@@ -922,7 +933,7 @@ Qed.
 
 Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A).
 Proof.
-repeat red. intros.
+repeat red. intros x y ?.
 rewrite <- (app_nil_r (rev x)), <- (app_nil_r (rev y)).
 apply eqlistA_rev_app; auto.
 Qed.
@@ -936,15 +947,15 @@ Qed.
 Lemma SortA_equivlistA_eqlistA : forall l l',
    SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
 Proof.
-induction l; destruct l'; simpl; intros; auto.
-destruct (H1 a); assert (InA a nil) by auto; inv.
+intros l; induction l as [|a l IHl]; intros l'; destruct l' as [|a0 l']; simpl; intros H H0 H1; auto.
+destruct (H1 a0); assert (InA a0 nil) by auto; inv.
 destruct (H1 a); assert (InA a nil) by auto; inv.
 inv.
 assert (forall y, InA y l -> ltA a y).
-intros; eapply SortA_InfA_InA with (l:=l); eauto.
+intros; eapply (SortA_InfA_InA (l:=l)); eauto.
 assert (forall y, InA y l' -> ltA a0 y).
-intros; eapply SortA_InfA_InA with (l:=l'); eauto.
-clear H3 H4.
+intros; eapply (SortA_InfA_InA (l:=l')); eauto.
+do 2 match goal with H : InfA _ _ |- _ => clear H end.
 assert (eqA a a0).
  destruct (H1 a).
  destruct (H1 a0).
@@ -953,13 +964,19 @@ assert (eqA a a0).
  elim (StrictOrder_Irreflexive a); eauto.
 constructor; auto.
 apply IHl; auto.
-split; intros.
+intros x; split; intros.
 destruct (H1 x).
 assert (InA x (a0::l')) by auto. inv; auto.
-rewrite H9,<-H3 in H4. elim (StrictOrder_Irreflexive a); eauto.
+match goal with H3 : eqA a a0, H4 : InA x l, H9 : eqA x a0 |- InA x l' =>
+  rewrite H9,<-H3 in H4
+end.
+elim (StrictOrder_Irreflexive a); eauto.
 destruct (H1 x).
 assert (InA x (a::l)) by auto. inv; auto.
-rewrite H9,H3 in H4. elim (StrictOrder_Irreflexive a0); eauto.
+match goal with H3 : eqA a a0, H4 : InA x l', H9 : eqA x a |- InA x l =>
+  rewrite H9,H3 in H4
+end.
+elim (StrictOrder_Irreflexive a0); eauto.
 Qed.
 
 End EqlistA.
@@ -970,12 +987,12 @@ Section Filter.
 
 Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l).
 Proof.
-induction l; simpl; auto.
+intros f l; induction l as [|a l IHl]; simpl; auto.
 intros; inv; auto.
 destruct (f a); auto.
 constructor; auto.
 apply In_InfA; auto.
-intros.
+intros y H.
 rewrite filter_In in H; destruct H.
 eapply SortA_InfA_InA; eauto.
 Qed.
@@ -984,12 +1001,14 @@ Arguments eq {A} x _.
 Lemma filter_InA : forall f, Proper (eqA==>eq) f ->
  forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
 Proof.
+(* Unset Mangle Names. *)
 clear sotrans ltA ltA_strorder ltA_compat.
-intros; do 2 rewrite InA_alt; intuition.
-destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
-destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition.
+intros f H l x; do 2 rewrite InA_alt; intuition;
+  match goal with Hex' : exists _, _ |- _ => rename Hex' into Hex end.
+destruct Hex as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
+destruct Hex as (y,(H0,H1)); rewrite filter_In in H1; intuition.
   rewrite (H _ _ H0); auto.
-destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition.
+destruct Hex as (y,(H0,H1)); exists y; rewrite filter_In; intuition.
   rewrite <- (H _ _ H0); auto.
 Qed.
 
@@ -997,19 +1016,20 @@ Lemma filter_split :
  forall f, (forall x y, f x = true -> f y = false -> ltA x y) ->
  forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l.
 Proof.
-induction l; simpl; intros; auto.
+intros f H l; induction l as [|a l IHl]; simpl; intros H0; auto.
 inv.
+match goal with H1' : SortA l, H2' : InfA a l |- _ => rename H1' into H1, H2' into H2 end.
 rewrite IHl at 1; auto.
 case_eq (f a); simpl; intros; auto.
-assert (forall e, In e l -> f e = false).
-  intros.
+assert (forall e, In e l -> f e = false) as H3.
+  intros e H3.
   assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)).
   case_eq (f e); simpl; intros; auto.
   elim (StrictOrder_Irreflexive e).
   transitivity a; auto.
 replace (List.filter f l) with (@nil A); auto.
-generalize H3; clear; induction l; simpl; auto.
-case_eq (f a); auto; intros.
+generalize H3; clear; induction l as [|a l IHl]; simpl; auto.
+case_eq (f a); auto; intros H H3.
 rewrite H3 in H; auto; try discriminate.
 Qed.
 
@@ -1043,23 +1063,24 @@ Lemma findA_NoDupA :
 Proof.
 set (eqk := fun p p' : A*B => eqA (fst p) (fst p')).
 set (eqke := fun p p' : A*B => eqA (fst p) (fst p') /\ snd p = snd p').
-induction l; intros; simpl.
-split; intros; try discriminate.
+intros l; induction l as [|a l IHl]; intros a0 b H; simpl.
+split; intros H0; try discriminate.
 invlist InA.
 destruct a as (a',b'); rename a0 into a.
 invlist NoDupA.
 split; intros.
 invlist InA.
-compute in H2; destruct H2. subst b'.
+match goal with H2 : eqke (a, b) (a', b') |- _ => compute in H2; destruct H2 end.
+subst b'.
 destruct (eqA_dec a a'); intuition.
 destruct (eqA_dec a a') as [HeqA|]; simpl.
-contradict H0.
-revert HeqA H2; clear - eqA_equiv.
+match goal with H0 : ~ InA eqk (a', b') l |- _ => contradict H0 end.
+match goal with H2 : InA eqke (a, b) l |- _ => revert HeqA H2; clear - eqA_equiv end.
 induction l.
 intros; invlist InA.
 intros; invlist InA; auto.
-destruct a0.
-compute in H; destruct H.
+match goal with |- InA eqk _ (?p :: _) => destruct p as [a0 b0] end.
+match goal with H : eqke (a, b) (a0, b0) |- _ => compute in H; destruct H end.
 subst b.
 left; auto.
 compute.
diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v
index 131668154e..7560ea96b5 100644
--- a/theories/Logic/ProofIrrelevanceFacts.v
+++ b/theories/Logic/ProofIrrelevanceFacts.v
@@ -27,7 +27,7 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance).
       forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p),
         x = eq_rect p Q x p h.
     Proof.
-      intros; rewrite M.proof_irrelevance with (p1:=h) (p2:=eq_refl p).
+      intros U p Q x h; rewrite (M.proof_irrelevance _ h (eq_refl p)).
       reflexivity.
     Qed.
   End Eq_rect_eq.
@@ -45,8 +45,8 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance).
     forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y),
       x = y -> exist P x p = exist P y q.
   Proof.
-    intros.
-    rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H).
+    intros U P x y p q H.
+    rewrite (M.proof_irrelevance _ q (eq_rect x P p y H)).
     elim H using eq_indd.
     reflexivity.
   Qed.
@@ -55,8 +55,8 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance).
     forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y),
       x = y -> existT P x p = existT P y q.
   Proof.
-    intros.
-    rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H).
+    intros U P x y p q H.
+    rewrite (M.proof_irrelevance _ q (eq_rect x P p y H)).
     elim H using eq_indd.
     reflexivity.
   Qed.
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 9788ad50dc..9540bc1075 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -68,10 +68,11 @@ Ltac pi := repeat f_equal ; apply proof_irrelevance.
 
 Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> `n = `m.
 Proof.
+  intros A P n m.
   destruct n as (x,p).
   destruct m as (x',p').
   simpl.
-  split ; intros ; subst.
+  split ; intros H ; subst.
 
   - inversion H.
     reflexivity.
@@ -92,7 +93,7 @@ Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B)
   (y : {y:A | y = x}),
   match_eq A B x fn = fn y.
 Proof.
-  intros.
+  intros A B x fn y.
   unfold match_eq.
   f_equal.
   destruct y.
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
index 206eb606d2..422316d879 100644
--- a/theories/Sorting/Sorted.v
+++ b/theories/Sorting/Sorted.v
@@ -71,6 +71,7 @@ Section defs.
       (forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) ->
       forall l:list A, Sorted l -> P l.
   Proof.
+    intros P ? ? l.
     induction l. firstorder using Sorted_inv. firstorder using Sorted_inv.
   Qed.
 
@@ -78,7 +79,8 @@ Section defs.
   Proof.
     split; [induction 1 as [|a l [|]]| induction 1];
       auto using Sorted, LocallySorted, HdRel.
-    inversion H1; subst; auto using LocallySorted.
+    match goal with H1 : HdRel a (_ :: _) |- _ => inversion H1 end.
+    subst; auto using LocallySorted.
   Qed.
 
   (** Strongly sorted: elements of the list are pairwise ordered *)
@@ -90,7 +92,7 @@ Section defs.
   Lemma StronglySorted_inv : forall a l, StronglySorted (a :: l) ->
     StronglySorted l /\ Forall (R a) l.
   Proof.
-    intros; inversion H; auto.
+    intros a l H; inversion H; auto.
   Defined.
 
   Lemma StronglySorted_rect :
@@ -99,7 +101,7 @@ Section defs.
       (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) ->
       forall l, StronglySorted l -> P l.
   Proof.
-    induction l; firstorder using StronglySorted_inv.
+    intros P ? ? l; induction l; firstorder using StronglySorted_inv.
   Defined.
 
   Lemma StronglySorted_rec :
@@ -120,7 +122,8 @@ Section defs.
   Lemma Sorted_extends :
     Transitive R -> forall a l, Sorted (a::l) -> Forall (R a) l.
   Proof.
-    intros. change match a :: l with [] => True | a :: l => Forall (R a) l end.
+    intros H a l H0.
+    change match a :: l with [] => True | a :: l => Forall (R a) l end.
     induction H0 as [|? ? ? ? H1]; [trivial|].
     destruct H1; constructor; trivial.
     eapply Forall_impl; [|eassumption].
diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index c923b503a7..a49e21fa92 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -93,7 +93,7 @@ Module KeyDecidableType(D:DecidableType).
 
   Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
   Proof.
-   intros; apply InA_eqA with p; auto using eqk_equiv.
+   intros p q m **; apply InA_eqA with p; auto using eqk_equiv.
   Qed.
 
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
@@ -106,18 +106,18 @@ Module KeyDecidableType(D:DecidableType).
 
   Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
   Proof.
-  firstorder.
-  exists x; auto.
-  induction H.
-  destruct y.
-  exists e; auto.
-  destruct IHInA as [e H0].
+  intros k l; split; intros [y H].
+  exists y; auto.
+  induction H as [a l eq|a l H IH].
+  destruct a as [k' y'].
+  exists y'; auto.
+  destruct IH as [e H0].
   exists e; auto.
   Qed.
 
   Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
   Proof.
-    intros; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv.
+    intros l x y e **; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv.
   Qed.
 
   Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
@@ -127,21 +127,21 @@ Module KeyDecidableType(D:DecidableType).
 
   Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
   Proof.
-    inversion 1.
-    inversion_clear H0; eauto.
+    inversion 1 as [? H0].
+    inversion_clear H0 as [? ? H1|]; eauto.
     destruct H1; simpl in *; intuition.
   Qed.
 
   Lemma In_inv_2 : forall k k' e e' l,
       InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
   Proof.
-   inversion_clear 1; compute in H0; intuition.
+   inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition.
   Qed.
 
   Lemma In_inv_3 : forall x x' l,
       InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
   Proof.
-   inversion_clear 1; compute in H0; intuition.
+   inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition.
   Qed.
 
  End Elt.
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index dc7a48cd6b..7bc9f97e2b 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -65,7 +65,7 @@ Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType.
 
   Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
   Proof with auto with ordered_type.
-   intros; elim (compare x y); intro H; [ right | left | right ]...
+   intros x y; elim (compare x y); intro H; [ right | left | right ]...
    assert (~ eq y x)...
   Defined.
 
@@ -83,7 +83,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
 
   Lemma lt_antirefl : forall x, ~ lt x x.
   Proof.
-   intros; intro; absurd (eq x x); auto with ordered_type.
+   intros x; intro; absurd (eq x x); auto with ordered_type.
   Qed.
 
   Instance lt_strorder : StrictOrder lt.
@@ -91,14 +91,14 @@ Module OrderedTypeFacts (Import O: OrderedType).
 
   Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
   Proof with auto with ordered_type.
-   intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto.
+   intros x y z H ?; destruct (compare x z) as [Hlt|Heq|Hlt]; auto.
    elim (lt_not_eq H); apply eq_trans with z...
    elim (lt_not_eq (lt_trans Hlt H))...
   Qed.
 
   Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.
   Proof with auto with ordered_type.
-   intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto.
+   intros x y z H H0; destruct (compare x z) as [Hlt|Heq|Hlt]; auto.
    elim (lt_not_eq H0); apply eq_trans with x...
    elim (lt_not_eq (lt_trans H0 Hlt))...
   Qed.
@@ -111,7 +111,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
   Qed.
 
   Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
-  Proof. intros; destruct (compare x y); auto. Qed.
+  Proof. intros x y; destruct (compare x y); auto. Qed.
 
   Module TO.
    Definition t := t.
@@ -157,7 +157,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
    forall x y : t,
    eq x y -> exists H : eq x y, compare x y = EQ H.
   Proof.
-   intros; case (compare x y); intros H'; try (exfalso; order).
+   intros x y H; case (compare x y); intros H'; try (exfalso; order).
    exists H'; auto.
   Qed.
 
@@ -165,7 +165,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
    forall x y : t,
    lt x y -> exists H : lt x y, compare x y = LT H.
   Proof.
-   intros; case (compare x y); intros H'; try (exfalso; order).
+   intros x y H; case (compare x y); intros H'; try (exfalso; order).
    exists H'; auto.
   Qed.
 
@@ -173,7 +173,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
    forall x y : t,
    lt y x -> exists H : lt y x, compare x y = GT H.
   Proof.
-   intros; case (compare x y); intros H'; try (exfalso; order).
+   intros x y H; case (compare x y); intros H'; try (exfalso; order).
    exists H'; auto.
   Qed.
 
@@ -203,7 +203,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
 
   Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.
   Proof.
-   intros; elim (compare x y); [ left | right | right ]; auto with ordered_type.
+   intros x y; elim (compare x y); [ left | right | right ]; auto with ordered_type.
   Defined.
 
   Definition eqb x y : bool := if eq_dec x y then true else false.
@@ -211,7 +211,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
   Lemma eqb_alt :
     forall x y, eqb x y = match compare x y with EQ _ => true | _ => false end.
   Proof.
-  unfold eqb; intros; destruct (eq_dec x y); elim_comp; auto.
+  unfold eqb; intros x y; destruct (eq_dec x y); elim_comp; auto.
   Qed.
 
 (* Specialization of results about lists modulo. *)
@@ -327,7 +327,7 @@ Module KeyOrderedType(O:OrderedType).
   Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.
   Proof.
     unfold eqke, ltk; intuition; simpl in *; subst.
-    exact (lt_not_eq H H1).
+    match goal with H : lt _ _, H1 : eq _ _ |- _ => exact (lt_not_eq H H1) end.
   Qed.
 
   #[local]
@@ -398,18 +398,18 @@ Module KeyOrderedType(O:OrderedType).
 
   Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
   Proof with auto with ordered_type.
-  firstorder.
-    exists x...
-  induction H.
-    destruct y.
-    exists e...
-  destruct IHInA as [e H0].
+  intros k l; split; intros [y H].
+    exists y...
+  induction H as [a l eq|a l H IH].
+    destruct a as [k' y'].
+    exists y'...
+  destruct IH as [e H0].
   exists e...
   Qed.
 
   Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
   Proof.
-  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *.
+  intros l x y e **; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *.
   Qed.
 
   Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
@@ -437,7 +437,7 @@ Module KeyOrderedType(O:OrderedType).
   Lemma Sort_Inf_NotIn :
       forall l k e, Sort l -> Inf (k,e) l ->  ~In k l.
   Proof.
-    intros; red; intros.
+    intros l k e H H0; red; intros H1.
     destruct H1 as [e' H2].
     elim (@ltk_not_eqk (k,e) (k,e')).
     eapply Sort_Inf_In; eauto with ordered_type.
@@ -457,34 +457,34 @@ Module KeyOrderedType(O:OrderedType).
   Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) ->
       ltk e e' \/ eqk e e'.
   Proof.
-    inversion_clear 2; auto with ordered_type.
+    intros l; inversion_clear 2; auto with ordered_type.
     left; apply Sort_In_cons_1 with l; auto.
   Qed.
 
   Lemma Sort_In_cons_3 :
     forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k.
   Proof.
-    inversion_clear 1; red; intros.
+    inversion_clear 1 as [|? ? H0 H1]; red; intros H H2.
     destruct (Sort_Inf_NotIn H0 H1 (In_eq H2 H)).
   Qed.
 
   Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
   Proof.
-    inversion 1.
-    inversion_clear H0; eauto with ordered_type.
+    inversion 1 as [? H0].
+    inversion_clear H0 as [? ? H1|]; eauto with ordered_type.
     destruct H1; simpl in *; intuition.
   Qed.
 
   Lemma In_inv_2 : forall k k' e e' l,
       InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
   Proof.
-   inversion_clear 1; compute in H0; intuition.
+   inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition.
   Qed.
 
   Lemma In_inv_3 : forall x x' l,
       InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
   Proof.
-   inversion_clear 1; compute in H0; intuition.
+   inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition.
   Qed.
 
  End Elt.