Made option "Automatic Introduction" active by default before too many

people use the undocumented "Lemma foo x : t" feature in a way
incompatible with this activation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7

26 files changed, 115 insertions, 117 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index cb87e2f2b..28d8cd07b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -61,7 +61,7 @@ let verbosely f x = without_option silent f x
 let if_silent f x = if !silent then f x
 let if_verbose f x = if not !silent then f x
 
-let auto_intros = ref false
+let auto_intros = ref true
 let make_auto_intros flag = auto_intros := flag
 let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros
 
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 598b21d83..626841be8 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -94,7 +94,7 @@ Theorem refl_pos_eq : forall m, pos_eq m m = true.
 induction m;simpl;auto.
 Qed.
 
-Definition pos_eq_dec (m n:positive) :{m=n}+{m<>n} .
+Definition pos_eq_dec : forall (m n:positive), {m=n}+{m<>n} .
 fix 1;intros [mm|mm|] [nn|nn|];try (right;congruence).
 case (pos_eq_dec mm nn).
 intro e;left;apply (f_equal xI e).
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 635b72671..9db022515 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -22,7 +22,7 @@ Defined.
 
 Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}.
 Proof.
-  induction n; destruct m; auto with arith.
+  induction n in m |- *; destruct m; auto with arith.
   destruct (IHn m) as [H|H]; auto with arith.
   destruct H; auto with arith.
 Defined.
@@ -34,7 +34,7 @@ Defined.
 
 Definition le_lt_dec n m : {n <= m} + {m < n}.
 Proof.
-  induction n.
+  induction n in m |- *.
   auto with arith.
   destruct m.
   auto with arith.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 2421c90d0..f21439107 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -476,8 +476,7 @@ Qed.
 
 Lemma proper_normalizes_proper `(Normalizes A R0 R1, Proper A R1 m) : Proper R0 m.
 Proof.
-  intros A R0 R1 H m H'.
-  red in H, H'.
+  red in H, H0.
   setoid_rewrite H.
   assumption.
 Qed.
@@ -512,16 +511,16 @@ Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances.
 (** When the relation on the domain is symmetric, we can
     inverse the relation on the codomain. Same for binary functions. *)
 
-Lemma proper_sym_flip
- `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f) :
+Lemma proper_sym_flip :
+ forall `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f),
  Proper (R1==>inverse R2) f.
 Proof.
 intros A R1 Sym B R2 f Hf.
 intros x x' Hxx'. apply Hf, Sym, Hxx'.
 Qed.
 
-Lemma proper_sym_flip_2
- `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f) :
+Lemma proper_sym_flip_2 :
+ forall `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f),
  Proper (R1==>R2==>inverse R3) f.
 Proof.
 intros A R1 Sym1 B R2 Sym2 C R3 f Hf.
@@ -532,14 +531,14 @@ Qed.
   compatible with [iff] as soon as it is compatible with [impl].
   Same with a binary relation. *)
 
-Lemma proper_sym_impl_iff `(Symmetric A R)`(Proper _ (R==>impl) f) :
+Lemma proper_sym_impl_iff : forall `(Symmetric A R)`(Proper _ (R==>impl) f),
  Proper (R==>iff) f.
 Proof.
 intros A R Sym f Hf x x' Hxx'. repeat red in Hf. split; eauto.
 Qed.
 
-Lemma proper_sym_impl_iff_2
- `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>impl) f) :
+Lemma proper_sym_impl_iff_2 :
+ forall `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>impl) f),
  Proper (R==>R'==>iff) f.
 Proof.
 intros A R Sym B R' Sym' f Hf x x' Hxx' y y' Hyy'.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index fd01495c4..7972c96ca 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -134,13 +134,13 @@ Proof. firstorder. Qed.
 Instance fst_compat { A B } (RA:relation A)(RB:relation B) :
  Proper (RA*RB ==> RA) Fst.
 Proof.
-intros A B RA RB (x,y) (x',y') (Hx,Hy); compute in *; auto.
+intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
 Qed.
 
 Instance snd_compat { A B } (RA:relation A)(RB:relation B) :
  Proper (RA*RB ==> RB) Snd.
 Proof.
-intros A B RA RB (x,y) (x',y') (Hx,Hy); compute in *; auto.
+intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
 Qed.
 
 Instance RelCompFun_compat {A B}(f:A->B)(R : relation B)
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index e0ddbe3ab..f9dda5125 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -2107,7 +2107,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Definition compare (s s':t) : Compare lt eq s s'.
   Proof.
-   intros (s,b) (s',b').
+   destruct s as (s,b), s' as (s',b').
    generalize (compare_Cmp s s').
    destruct compare_pure; intros; [apply EQ|apply LT|apply GT]; red; auto.
   Defined.
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 1facce290..774bcd9b3 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -736,7 +736,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Definition compare (s s':t) : Compare lt eq s s'.
   Proof.
-   intros (s,b,a) (s',b',a').
+   destruct s as (s,b,a), s' as (s',b',a').
    generalize (compare_Cmp s s').
    destruct compare_aux; intros; [apply EQ|apply LT|apply GT]; red; auto.
   Defined.
diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v
index 5d6a4f7d6..60b71ca33 100644
--- a/theories/Logic/FunctionalExtensionality.v
+++ b/theories/Logic/FunctionalExtensionality.v
@@ -52,5 +52,5 @@ Qed.
 
 Lemma eta_expansion {A B} (f : A -> B) : f = fun x => f x.
 Proof.
-  intros A B f. apply (eta_expansion_dep f).
+  apply (eta_expansion_dep f).
 Qed.
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 0d24e0339..d8486180c 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -833,7 +833,7 @@ Qed.
 Instance bal_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
  Ok (bal l x r).
 Proof.
- intros l x r; functional induction bal l x r; intros;
+ functional induction bal l x r; intros;
  inv; repeat apply create_ok; auto; unfold create;
  (apply lt_tree_node || apply gt_tree_node); auto;
  (eapply lt_tree_trans || eapply gt_tree_trans); eauto.
@@ -894,7 +894,7 @@ Proof.
  apply create_spec.
 Qed.
 
-Instance join_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
+Instance join_ok : forall l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r),
  Ok (join l x r).
 Proof.
  join_tac; auto with *; inv; apply bal_ok; auto;
@@ -915,10 +915,10 @@ Proof.
  rewrite bal_spec, In_node_iff, IHp, e0; simpl; intuition.
 Qed.
 
-Instance remove_min_ok l x r h `(Ok (Node l x r h)) :
+Instance remove_min_ok l x r : forall h `(Ok (Node l x r h)),
  Ok (remove_min l x r)#1.
 Proof.
- intros l x r; functional induction (remove_min l x r); simpl; intros.
+ functional induction (remove_min l x r); simpl; intros.
  inv; auto.
  assert (O : Ok (Node ll lx lr _x)) by (inv; auto).
  assert (L : lt_tree x (Node ll lx lr _x)) by (inv; auto).
@@ -958,11 +958,11 @@ Proof.
  rewrite bal_spec, remove_min_spec, e1; simpl; intuition.
 Qed.
 
-Instance merge_ok s1 s2 `(Ok s1, Ok s2)
- `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2) :
+Instance merge_ok s1 s2 : forall `(Ok s1, Ok s2)
+ `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2),
  Ok (merge s1 s2).
 Proof.
- intros s1 s2; functional induction (merge s1 s2); intros; auto;
+ functional induction (merge s1 s2); intros; auto;
  try factornode _x _x0 _x1 _x2 as s1.
  apply bal_ok; auto.
  change s2' with ((s2',m)#1); rewrite <-e1; eauto with *.
@@ -1110,11 +1110,11 @@ Proof.
  rewrite join_spec, remove_min_spec, e1; simpl; intuition.
 Qed.
 
-Instance concat_ok s1 s2 `(Ok s1, Ok s2)
- `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2) :
+Instance concat_ok s1 s2 : forall `(Ok s1, Ok s2)
+ `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2),
  Ok (concat s1 s2).
 Proof.
- intros s1 s2; functional induction (concat s1 s2); intros; auto;
+ functional induction (concat s1 s2); intros; auto;
  try factornode _x _x0 _x1 _x2 as s1.
  apply join_ok; auto.
  change (Ok (s2',m)#1); rewrite <-e1; eauto with *.
@@ -1164,7 +1164,7 @@ Proof.
  destruct (split x r); simpl in *. rewrite IHr; intuition_in; order.
 Qed.
 
-Lemma split_ok s x `{Ok s} : Ok (split x s)#l /\ Ok (split x s)#r.
+Lemma split_ok : forall s x `{Ok s}, Ok (split x s)#l /\ Ok (split x s)#r.
 Proof.
  induct s x; simpl; auto.
  specialize (IHl x).
@@ -1273,9 +1273,9 @@ Proof.
  elim_compare y x1; intuition_in.
 Qed.
 
-Instance union_ok s1 s2 `(Ok s1, Ok s2) : Ok (union s1 s2).
+Instance union_ok s1 s2 : forall `(Ok s1, Ok s2), Ok (union s1 s2).
 Proof.
- intros s1 s2; functional induction union s1 s2; intros B1 B2; auto.
+ functional induction union s1 s2; intros B1 B2; auto.
  factornode _x0 _x1 _x2 _x3 as s2; destruct_split; inv.
  apply join_ok; auto with *.
  intro y; rewrite union_spec, split_spec1; intuition_in.
@@ -1387,7 +1387,7 @@ Proof.
  rewrite H0 in H3; discriminate.
 Qed.
 
-Instance filter_ok' s acc f `(Ok s, Ok acc) :
+Instance filter_ok' : forall s acc f `(Ok s, Ok acc),
  Ok (filter_acc f acc s).
 Proof.
  induction s; simpl; auto.
@@ -1473,7 +1473,7 @@ Proof.
  intros u v H; rewrite H; auto.
 Qed.
 
-Instance partition_ok1' s acc f `(Ok s, Ok acc#1) :
+Instance partition_ok1' : forall s acc f `(Ok s, Ok acc#1),
  Ok (partition_acc f acc s)#1.
 Proof.
  induction s; simpl; auto.
@@ -1484,7 +1484,7 @@ Proof.
  apply IHs1; simpl; auto with *.
 Qed.
 
-Instance partition_ok2' s acc f `(Ok s, Ok acc#2) :
+Instance partition_ok2' : forall s acc f `(Ok s, Ok acc#2),
  Ok (partition_acc f acc s)#2.
 Proof.
  induction s; simpl; auto.
@@ -1496,10 +1496,10 @@ Proof.
 Qed.
 
 Instance partition_ok1 s f `(Ok s) : Ok (partition f s)#1.
-Proof. intros; apply partition_ok1'; auto. Qed.
+Proof. apply partition_ok1'; auto. Qed.
 
 Instance partition_ok2 s f `(Ok s) : Ok (partition f s)#2.
-Proof. intros; apply partition_ok2'; auto. Qed.
+Proof. apply partition_ok2'; auto. Qed.
 
 
 
diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v
index b61bf3fe7..4e17618f7 100644
--- a/theories/MSets/MSetFacts.v
+++ b/theories/MSets/MSetFacts.v
@@ -488,13 +488,13 @@ Qed.
 
 Generalizable Variables f.
 
-Instance filter_equal `(Proper _ (E.eq==>Logic.eq) f) :
+Instance filter_equal : forall `(Proper _ (E.eq==>Logic.eq) f),
  Proper (Equal==>Equal) (filter f).
 Proof.
 intros f Hf s s' Hs a. rewrite !filter_iff, Hs by auto; intuition.
 Qed.
 
-Instance filter_subset `(Proper _ (E.eq==>Logic.eq) f) :
+Instance filter_subset : forall `(Proper _ (E.eq==>Logic.eq) f),
  Proper (Subset==>Subset) (filter f).
 Proof.
 intros f Hf s s' Hs a. rewrite !filter_iff, Hs by auto; intuition.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index b73af8f1a..45278eaf6 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -328,9 +328,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Qed.
   Hint Resolve add_inf.
 
-  Global Instance add_ok s x `(Ok s) : Ok (add x s).
+  Global Instance add_ok s x : forall `(Ok s), Ok (add x s).
   Proof.
-  intros s x; repeat rewrite <- isok_iff; revert s x.
+  repeat rewrite <- isok_iff; revert s x.
   simple induction s; simpl.
   intuition.
   intros; elim_compare x a; inv; auto.
@@ -356,9 +356,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Qed.
   Hint Resolve remove_inf.
 
-  Global Instance remove_ok s x `(Ok s) : Ok (remove x s).
+  Global Instance remove_ok s x : forall `(Ok s), Ok (remove x s).
   Proof.
-  intros s x; repeat rewrite <- isok_iff; revert s x.
+  repeat rewrite <- isok_iff; revert s x.
   induction s; simpl.
   intuition.
   intros; elim_compare x a; inv; auto.
@@ -399,9 +399,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Qed.
   Hint Resolve union_inf.
 
-  Global Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s').
+  Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').
   Proof.
-  intros s s'; repeat rewrite <- isok_iff; revert s s'.
+  repeat rewrite <- isok_iff; revert s s'.
   induction2; constructors; try apply @ok; auto.
   apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto.
   change (Inf x' (union (x :: l) l')); auto.
@@ -426,9 +426,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Qed.
   Hint Resolve inter_inf.
 
-  Global Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
+  Global Instance inter_ok s s' : forall `(Ok s, Ok s'), Ok (inter s s').
   Proof.
-  intros s s'; repeat rewrite <- isok_iff; revert s s'.
+  repeat rewrite <- isok_iff; revert s s'.
   induction2.
   constructors; auto.
   apply Inf_eq with x'; auto; apply inter_inf; auto; apply Inf_eq with x; auto.
@@ -457,9 +457,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Qed.
   Hint Resolve diff_inf.
 
-  Global Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s').
+  Global Instance diff_ok s s' : forall `(Ok s, Ok s'), Ok (diff s s').
   Proof.
-  intros s s'; repeat rewrite <- isok_iff; revert s s'.
+  repeat rewrite <- isok_iff; revert s s'.
   induction2.
   Qed.
 
@@ -644,9 +644,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   apply Inf_lt with x; auto.
   Qed.
 
-  Global Instance filter_ok s f `(Ok s) : Ok (filter f s).
+  Global Instance filter_ok s f : forall `(Ok s), Ok (filter f s).
   Proof.
-  intros s f; repeat rewrite <- isok_iff; revert s f.
+  repeat rewrite <- isok_iff; revert s f.
   simple induction s; simpl.
   auto.
   intros x l Hrec f Hs; inv.
@@ -725,9 +725,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   auto.
   Qed.
 
-  Global Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
+  Global Instance partition_ok1 s f : forall `(Ok s), Ok (fst (partition f s)).
   Proof.
-  intros s f; repeat rewrite <- isok_iff; revert s f.
+  repeat rewrite <- isok_iff; revert s f.
   simple induction s; simpl.
   auto.
   intros x l Hrec f Hs; inv.
@@ -735,9 +735,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   case (f x); case (partition f l); simpl; auto.
   Qed.
 
-  Global Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).
+  Global Instance partition_ok2 s f : forall `(Ok s), Ok (snd (partition f s)).
   Proof.
-  intros s f; repeat rewrite <- isok_iff; revert s f.
+  repeat rewrite <- isok_iff; revert s f.
   simple induction s; simpl.
   auto.
   intros x l Hrec f Hs; inv.
diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v
index 14fe097a9..9cd28e171 100644
--- a/theories/MSets/MSetProperties.v
+++ b/theories/MSets/MSetProperties.v
@@ -947,12 +947,12 @@ Module OrdProperties (M:Sets).
 
   Instance gtb_compat x : Proper (E.eq==>Logic.eq) (gtb x).
   Proof.
-   intros x a b H. unfold gtb. rewrite H; auto.
+   intros a b H. unfold gtb. rewrite H; auto.
   Qed.
 
   Instance leb_compat x : Proper (E.eq==>Logic.eq) (leb x).
   Proof.
-   intros x a b H; unfold leb. rewrite H; auto.
+   intros a b H; unfold leb. rewrite H; auto.
   Qed.
   Hint Resolve gtb_compat leb_compat.
 
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 8239ecef8..799e5f57e 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -275,7 +275,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   reflexivity.
   Qed.
 
-  Global Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s').
+  Global Instance union_ok : forall s s' `(Ok s, Ok s'), Ok (union s s').
   Proof.
   induction s; simpl; auto; intros; inv; unfold flip; auto with *.
   Qed.
@@ -291,7 +291,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
 
   Global Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
   Proof.
-  unfold inter, fold, flip; intros s.
+  unfold inter, fold, flip.
   set (acc := nil (A:=elt)).
   assert (Hacc : Ok acc) by constructors.
   clearbody acc; revert acc Hacc.
@@ -322,7 +322,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   rewrite H2, <- mem_spec in H3; auto. congruence.
   Qed.
 
-  Global Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s').
+  Global Instance diff_ok : forall s s' `(Ok s, Ok s'), Ok (diff s s').
   Proof.
   unfold diff; intros s s'; revert s.
   induction s'; simpl; unfold flip; auto; intros. inv; auto with *.
@@ -491,7 +491,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   inversion_clear H; auto.
   Qed.
 
-  Global Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
+  Global Instance partition_ok1 : forall s f `(Ok s), Ok (fst (partition f s)).
   Proof.
   simple induction s; simpl.
   auto.
@@ -501,7 +501,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   case (f x); case (partition f l); simpl; constructors; auto.
   Qed.
 
-  Global Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).
+  Global Instance partition_ok2 : forall s f `(Ok s), Ok (snd (partition f s)).
   Proof.
   simple induction s; simpl.
   auto.
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index a79cfac3d..ea53c7d06 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -685,7 +685,7 @@ Qed.
 
 Definition Bnth (n:nat)(bv:Bvector n)(p:nat) : p<n -> bool.
 Proof.
- induction 1.
+ induction bv in p |- *.
  intros.
  exfalso; inversion H.
  intros.
diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index f11fb67b1..558d452bb 100644
--- a/theories/Numbers/BigNumPrelude.v
+++ b/theories/Numbers/BigNumPrelude.v
@@ -331,7 +331,7 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
  Theorem Zgcd_div_pos a b:
    0 < b -> 0 < Zgcd a b -> 0 < b / Zgcd a b.
  Proof.
- intros a b Ha Hg.
+ intros Ha Hg.
  case (Zle_lt_or_eq 0 (b/Zgcd a b)); auto.
  apply Z_div_pos; auto with zarith.
  intros H; generalize Ha.
@@ -343,7 +343,7 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
  Theorem Zdiv_neg a b:
    a < 0 -> 0 < b -> a / b < 0.
  Proof.
- intros a b Ha Hb.
+ intros Ha Hb.
  assert (b > 0) by omega.
  generalize (Z_mult_div_ge a _ H); intros.
  assert (b * (a / b) < 0)%Z.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index ca73a9f00..668fe83d6 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1877,14 +1877,14 @@ Section Int31_Specs.
 
  Lemma quotient_by_2 a: a - 1 <= (a/2) + (a/2).
  Proof.
- intros a; case (Z_mod_lt a 2); auto with zarith.
+ case (Z_mod_lt a 2); auto with zarith.
  intros H1; rewrite Zmod_eq_full; auto with zarith.
  Qed.
 
  Lemma sqrt_main_trick j k: 0 <= j -> 0 <= k ->
    (j * k) + j <= ((j + k)/2 + 1)  ^ 2.
  Proof.
- intros j k Hj; generalize Hj k; pattern j; apply natlike_ind;
+ intros Hj; generalize Hj k; pattern j; apply natlike_ind;
    auto; clear k j Hj.
  intros _ k Hk; repeat rewrite Zplus_0_l.
  apply  Zmult_le_0_compat; generalize (Z_div_pos k 2); auto with zarith.
@@ -1907,7 +1907,7 @@ Section Int31_Specs.
 
  Lemma sqrt_main i j: 0 <= i -> 0 < j -> i < ((j + (i/j))/2 + 1) ^ 2.
  Proof.
- intros i j Hi Hj.
+ intros Hi Hj.
  assert (Hij: 0 <= i/j) by (apply Z_div_pos; auto with zarith).
  apply Zlt_le_trans with (2 := sqrt_main_trick _ _ (Zlt_le_weak _ _ Hj) Hij).
  pattern i at 1; rewrite (Z_div_mod_eq i j); case (Z_mod_lt i j); auto with zarith.
@@ -1915,7 +1915,7 @@ Section Int31_Specs.
 
  Lemma sqrt_init i: 1 < i -> i < (i/2 + 1) ^ 2.
  Proof.
- intros i Hi.
+ intros Hi.
  assert (H1: 0 <= i - 2) by auto with zarith.
  assert (H2: 1 <= (i / 2) ^ 2); auto with zarith.
    replace i with (1* 2 + (i - 2)); auto with zarith.
@@ -1933,14 +1933,14 @@ Section Int31_Specs.
 
  Lemma sqrt_test_true i j: 0 <= i -> 0 < j -> i/j >= j -> j ^ 2 <= i.
  Proof.
- intros i j Hi Hj Hd; rewrite Zpower_2.
+ intros Hi Hj Hd; rewrite Zpower_2.
  apply Zle_trans with (j * (i/j)); auto with zarith.
  apply Z_mult_div_ge; auto with zarith.
  Qed.
 
  Lemma sqrt_test_false i j: 0 <= i -> 0 < j -> i/j < j ->  (j + (i/j))/2 < j.
  Proof.
- intros i j Hi Hj H; case (Zle_or_lt j ((j + (i/j))/2)); auto.
+ intros Hi Hj H; case (Zle_or_lt j ((j + (i/j))/2)); auto.
  intros H1; contradict H; apply Zle_not_lt.
  assert (2 * j <= j + (i/j)); auto with zarith.
  apply Zle_trans with (2 * ((j + (i/j))/2)); auto with zarith.
@@ -1955,7 +1955,7 @@ Section Int31_Specs.
 
  Lemma Zcompare_spec i j: ZcompareSpec i j (i ?= j).
  Proof.
- intros i j; case_eq (Zcompare i j); intros H.
+ case_eq (Zcompare i j); intros H.
  apply ZcompareSpecEq; apply Zcompare_Eq_eq; auto.
  apply ZcompareSpecLt; auto.
  apply ZcompareSpecGt; apply Zgt_lt; auto.
@@ -1968,12 +1968,12 @@ Section Int31_Specs.
    | _ =>  j
    end.
  Proof.
- intros rec i j; unfold sqrt31_step; case div31; intros.
+ unfold sqrt31_step; case div31; intros.
  simpl; case compare31; auto.
  Qed.
 
  Lemma div31_phi i j: 0 < [|j|] -> [|fst (i/j)%int31|] = [|i|]/[|j|].
- intros i j Hj; generalize (spec_div i j Hj).
+ intros Hj; generalize (spec_div i j Hj).
  case div31; intros q r; simpl fst.
  intros (H1,H2); apply Zdiv_unique with [|r|]; auto with zarith.
  rewrite H1; ring.
@@ -1988,7 +1988,7 @@ Section Int31_Specs.
   [|sqrt31_step rec i j|] ^ 2 <= [|i|] < ([|sqrt31_step rec i j|] + 1) ^ 2.
  Proof.
  assert (Hp2: 0 < [|2|]) by exact (refl_equal Lt).
- intros rec i j Hi Hj Hij H31 Hrec; rewrite sqrt31_step_def.
+ intros Hi Hj Hij H31 Hrec; rewrite sqrt31_step_def.
  rewrite spec_compare, div31_phi; auto.
    case Zcompare_spec; auto; intros Hc;
    try (split; auto; apply sqrt_test_true; auto with zarith; fail).
@@ -2024,7 +2024,7 @@ Section Int31_Specs.
        [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) ->
   [|iter31_sqrt n rec i j|] ^ 2 <= [|i|] < ([|iter31_sqrt n rec i j|] + 1) ^ 2.
  Proof.
- intros n; elim n; unfold iter31_sqrt; fold iter31_sqrt; clear n.
+ revert rec i j; elim n; unfold iter31_sqrt; fold iter31_sqrt; clear n.
  intros rec i j Hi Hj Hij H31 Hrec; apply sqrt31_step_correct; auto with zarith.
  intros; apply Hrec; auto with zarith.
  rewrite Zpower_0_r; auto with zarith.
@@ -2083,14 +2083,14 @@ Section Int31_Specs.
        end
    end.
  Proof.
- intros rec ih il j; unfold sqrt312_step; case div3121; intros.
+ unfold sqrt312_step; case div3121; intros.
  simpl; case compare31; auto.
  Qed.
 
  Lemma sqrt312_lower_bound ih il j:
    phi2 ih  il  < ([|j|] + 1) ^ 2 -> [|ih|] <= [|j|].
  Proof.
- intros ih il j H1.
+ intros H1.
  case (phi_bounded j); intros Hbj _.
  case (phi_bounded il); intros Hbil _.
  case (phi_bounded ih); intros Hbih Hbih1.
@@ -2104,7 +2104,7 @@ Section Int31_Specs.
  Lemma div312_phi ih il j: (2^30 <= [|j|] -> [|ih|] < [|j|] ->
   [|fst (div3121 ih il j)|] = phi2 ih il/[|j|])%Z.
  Proof.
- intros ih il j Hj Hj1.
+ intros Hj Hj1.
  generalize (spec_div21 ih il j Hj Hj1).
  case div3121; intros q r (Hq, Hr).
  apply Zdiv_unique with (phi r); auto with zarith.
@@ -2119,7 +2119,7 @@ Section Int31_Specs.
       < ([|sqrt312_step rec ih il j|] + 1) ^  2.
  Proof.
  assert (Hp2: (0 < [|2|])%Z) by exact (refl_equal Lt).
- intros rec ih il j Hih Hj Hij Hrec; rewrite sqrt312_step_def.
+ intros Hih Hj Hij Hrec; rewrite sqrt312_step_def.
  assert (H1: ([|ih|] <= [|j|])%Z) by (apply sqrt312_lower_bound with il; auto).
  case (phi_bounded ih); intros Hih1 _.
  case (phi_bounded il); intros Hil1 _.
@@ -2213,7 +2213,7 @@ Section Int31_Specs.
   [|iter312_sqrt n rec ih il j|] ^ 2 <= phi2 ih il
       < ([|iter312_sqrt n rec ih il j|] + 1) ^ 2.
  Proof.
- intros n; elim n; unfold iter312_sqrt; fold iter312_sqrt; clear n.
+ revert rec ih il j; elim n; unfold iter312_sqrt; fold iter312_sqrt; clear n.
  intros rec ih il j Hi Hj Hij Hrec; apply sqrt312_step_correct; auto with zarith.
  intros; apply Hrec; auto with zarith.
  rewrite Zpower_0_r; auto with zarith.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index c0b8074b6..2eb8584c9 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -105,7 +105,7 @@ Qed.
 Theorem spec_to_N n:
  ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z.
 Proof.
-intros n; case n; simpl; intros p;
+case n; simpl; intros p;
   generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
 intros p1 H1; case H1; auto.
 intros p1 H1; case H1; auto.
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 7afbee4a4..05508c4f3 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -45,7 +45,7 @@ Qed.
 
 Global Instance iter_wd (R:relation A) : Proper ((R==>R)==>eq==>R==>R) iter.
 Proof.
-intros R f f' Hf n n' Hn; subst n'. induction n; simpl; red; auto.
+intros f f' Hf n n' Hn; subst n'. induction n; simpl; red; auto.
 Qed.
 
 End Iter.
@@ -412,4 +412,4 @@ Proof.
  rewrite ofnat_succ, pred_succ; auto with arith.
 Qed.
 
-End NZOfNatOps.
\ No newline at end of file
+End NZOfNatOps.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index ba592507b..a5ef02570 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -110,7 +110,7 @@ Implicit Arguments recursion [A].
 Instance recursion_wd A (Aeq : relation A) :
  Proper (Aeq==>(eq==>Aeq==>Aeq)==>eq==>Aeq) (@recursion A).
 Proof.
-intros A Aeq a a' Eaa' f f' Eff'.
+intros a a' Eaa' f f' Eff'.
 intro x; pattern x; apply Nrect.
 intros x' H; now rewrite <- H.
 clear x.
@@ -200,4 +200,4 @@ end.
 Time Eval vm_compute in (binlog 500000). (* 0 sec *)
 Time Eval vm_compute in (binlog 1000000000000000000000000000000). (* 0 sec *)
 
-*)
\ No newline at end of file
+*)
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 491c33666..5e3ecd688 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -126,7 +126,7 @@ Implicit Arguments recursion [A].
 Instance recursion_wd (A : Type) (Aeq : relation A) :
  Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
 Proof.
-intros A Aeq a a' Ha f f' Hf n n' Hn. subst n'.
+intros a a' Ha f f' Hf n n' Hn. subst n'.
 induction n; simpl; auto. apply Hf; auto.
 Qed.
 
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 8cbd96c1f..f4641446b 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -200,7 +200,7 @@ Instance recursion_wd (A : Type) (Aeq : relation A) :
  Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
 Proof.
 unfold eq.
-intros A Aeq a a' Eaa' f f' Eff' x x' Exx'.
+intros a a' Eaa' f f' Eff' x x' Exx'.
 unfold recursion.
 unfold N.to_N.
 rewrite <- Exx'; clear x' Exx'.
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 5022c9ae6..e2b63ebde 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -96,7 +96,7 @@ Definition predicate (A : Type) := A -> Prop.
 Instance well_founded_wd A :
  Proper (@relation_equivalence A ==> iff) (@well_founded A).
 Proof.
-intros A R1 R2 H.
+intros R1 R2 H.
 split; intros WF a; induction (WF a) as [x _ WF']; constructor;
 intros y Ryx; apply WF'; destruct (H y x); auto.
 Qed.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 6513922c4..407f7b90c 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -565,10 +565,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  ring.
  Qed.
 
- Instance strong_spec_mul_norm_Qz_Qq z n d
-   `(Reduced (Qq n d)) : Reduced (mul_norm_Qz_Qq z n d).
+ Instance strong_spec_mul_norm_Qz_Qq z n d :
+   forall `(Reduced (Qq n d)), Reduced (mul_norm_Qz_Qq z n d).
  Proof.
- unfold Reduced; intros z n d.
+ unfold Reduced.
  rewrite 2 strong_spec_red, 2 Qred_iff.
  simpl; nzsimpl.
  destr_eqb; intros Hd H; simpl in *; nzsimpl.
@@ -648,8 +648,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite <- Hg1, <- Hg2, <- Hg1', <- Hg2'; ring.
  Qed.
 
- Instance strong_spec_mul_norm x y
-  `(Reduced x, Reduced y) : Reduced (mul_norm x y).
+ Instance strong_spec_mul_norm x y :
+  forall `(Reduced x, Reduced y), Reduced (mul_norm x y).
  Proof.
  unfold Reduced; intros.
  rewrite strong_spec_red, Qred_iff.
@@ -833,7 +833,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  romega.
  Qed.
 
- Instance strong_spec_inv_norm x `(Reduced x) : Reduced (inv_norm x).
+ Instance strong_spec_inv_norm x : Reduced x -> Reduced (inv_norm x).
  Proof.
  unfold Reduced.
  intros.
@@ -888,7 +888,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_div x y: [div x y] == [x] / [y].
  Proof.
- intros x y; unfold div; rewrite spec_mul; auto.
+ unfold div; rewrite spec_mul; auto.
  unfold Qdiv; apply Qmult_comp.
  apply Qeq_refl.
  apply spec_inv; auto.
@@ -898,7 +898,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_div_norm x y: [div_norm x y] == [x] / [y].
  Proof.
- intros x y; unfold div_norm; rewrite spec_mul_norm; auto.
+ unfold div_norm; rewrite spec_mul_norm; auto.
  unfold Qdiv; apply Qmult_comp.
  apply Qeq_refl.
  apply spec_inv_norm; auto.
@@ -1019,8 +1019,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite spec_inv_norm, spec_power_pos; apply Qeq_refl.
  Qed.
 
- Instance strong_spec_power_norm x z
-   `(Reduced x) : Reduced (power_norm x z).
+ Instance strong_spec_power_norm x z :
+   Reduced x -> Reduced (power_norm x z).
  Proof.
  destruct z; simpl.
  intros _; unfold Reduced; rewrite strong_spec_red.
@@ -1088,7 +1088,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_addc x y:
   [[add x y]] = [[x]] + [[y]].
  Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x] + [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1102,7 +1102,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_add_normc x y:
   [[add_norm x y]] = [[x]] + [[y]].
  Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x] + [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1125,14 +1125,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_subc x y:  [[sub x y]] = [[x]] - [[y]].
  Proof.
- intros x y; unfold sub; rewrite spec_addc; auto.
+ unfold sub; rewrite spec_addc; auto.
  rewrite spec_oppc; ring.
  Qed.
 
  Theorem spec_sub_normc x y:
    [[sub_norm x y]] = [[x]] - [[y]].
  Proof.
- intros x y; unfold sub_norm; rewrite spec_add_normc; auto.
+ unfold sub_norm; rewrite spec_add_normc; auto.
  rewrite spec_oppc; ring.
  Qed.
 
@@ -1150,7 +1150,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_mulc x y:
   [[mul x y]] = [[x]] * [[y]].
  Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x] * [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1164,7 +1164,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_mul_normc x y:
    [[mul_norm x y]] = [[x]] * [[y]].
  Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x] * [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1188,7 +1188,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_invc x:
    [[inv x]] =  /[[x]].
  Proof.
- intros x; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! (/[x])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1202,7 +1202,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_inv_normc x:
    [[inv_norm x]] =  /[[x]].
  Proof.
- intros x; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! (/[x])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1225,14 +1225,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_divc x y: [[div x y]] = [[x]] / [[y]].
  Proof.
- intros x y; unfold div; rewrite spec_mulc; auto.
+ unfold div; rewrite spec_mulc; auto.
  unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto.
  apply spec_invc; auto.
  Qed.
 
  Theorem spec_div_normc x y: [[div_norm x y]] = [[x]] / [[y]].
  Proof.
- intros x y; unfold div_norm; rewrite spec_mul_normc; auto.
+ unfold div_norm; rewrite spec_mul_normc; auto.
  unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto.
  apply spec_inv_normc; auto.
  Qed.
@@ -1250,7 +1250,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_squarec x: [[square x]] = [[x]]^2.
  Proof.
- intros x; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x]^2)).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1267,7 +1267,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_power_posc x p:
    [[power_pos x p]] = [[x]] ^ nat_of_P p.
  Proof.
- intros x p; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x]^Zpos p)).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 717913572..3816c1505 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -134,7 +134,6 @@ Section Fix_rects.
             Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y)))))
     : forall x a, Q _ (Fix_F_sub A R P f x a).
   Proof with auto.
-    intros Q inv.
     set (R' := fun (x: A) => forall a, Q _ (Fix_F_sub A R P f x a)).
     cut (forall x, R' x)...
     apply (well_founded_induction_type Rwf).
@@ -167,7 +166,7 @@ Section Fix_rects.
     Fix_F_sub A R P f x a =
     Fix_F_sub A R P f x a'.
   Proof.
-    intros x a.
+    revert a'.
     pattern x, (Fix_F_sub A R P f x a).
     apply Fix_F_sub_rect.
     intros.
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index cf641253a..e5c08335d 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -16,15 +16,15 @@ Definition Setoid_Theory := @Equivalence.
 Definition Build_Setoid_Theory := @Build_Equivalence.
 
 Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x.
-  unfold Setoid_Theory. intros ; reflexivity.
+  unfold Setoid_Theory in s. intros ; reflexivity.
 Defined.
 
 Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x.
-  unfold Setoid_Theory. intros ; symmetry ; assumption.
+  unfold Setoid_Theory in s. intros ; symmetry ; assumption.
 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.
-  unfold Setoid_Theory. intros ; transitivity y ; assumption.
+  unfold Setoid_Theory in s. intros ; transitivity y ; assumption.
 Defined.
 
 (** Some tactics for manipulating Setoid Theory not officially
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 5faaebe28..acc7517dd 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -261,7 +261,7 @@ Qed.
 Global Instance if_eqA (B:Type)(b b':B) :
  Proper (eqA==>eqA==>@eq _) (fun x y => if eqA_dec x y then b else b').
 Proof.
- intros B b b' x x' Hxx' y y' Hyy'.
+ intros x x' Hxx' y y' Hyy'.
  intros; destruct (eqA_dec x y) as [H|H];
   destruct (eqA_dec x' y') as [H'|H']; auto.
  contradict H'; transitivity x; auto with *; transitivity y; auto with *.
@@ -292,7 +292,7 @@ Qed.
 Global Instance multiplicity_eqA (l:list A) :
  Proper (eqA==>@eq _) (multiplicity (list_contents l)).
 Proof.
-  intros l x x' Hxx'.
+  intros x x' Hxx'.
   induction l as [|y l Hl]; simpl; auto.
   rewrite (@if_eqA_rewrite_r y x x'); auto.
 Qed.