aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--lib/flags.ml2
-rw-r--r--plugins/rtauto/Bintree.v2
-rw-r--r--theories/Arith/Compare_dec.v4
-rw-r--r--theories/Classes/Morphisms.v17
-rw-r--r--theories/Classes/RelationPairs.v4
-rw-r--r--theories/FSets/FMapAVL.v2
-rw-r--r--theories/FSets/FMapFullAVL.v2
-rw-r--r--theories/Logic/FunctionalExtensionality.v2
-rw-r--r--theories/MSets/MSetAVL.v36
-rw-r--r--theories/MSets/MSetFacts.v4
-rw-r--r--theories/MSets/MSetList.v32
-rw-r--r--theories/MSets/MSetProperties.v4
-rw-r--r--theories/MSets/MSetWeakList.v10
-rw-r--r--theories/NArith/Ndigits.v2
-rw-r--r--theories/Numbers/BigNumPrelude.v4
-rw-r--r--theories/Numbers/Cyclic/Int31/Cyclic31.v32
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v2
-rw-r--r--theories/Numbers/NatInt/NZDomain.v4
-rw-r--r--theories/Numbers/Natural/Binary/NBinary.v4
-rw-r--r--theories/Numbers/Natural/Peano/NPeano.v2
-rw-r--r--theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v2
-rw-r--r--theories/Numbers/NumPrelude.v2
-rw-r--r--theories/Numbers/Rational/BigQ/QMake.v44
-rw-r--r--theories/Program/Wf.v3
-rw-r--r--theories/Setoids/Setoid.v6
-rw-r--r--theories/Sorting/PermutSetoid.v4
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.