3 files changed, 7 insertions, 7 deletions
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index f30c5b763..6b02e8383 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -162,7 +162,7 @@ Section Infinite_sets.
     generalize (H'3 x).
     intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
       auto with sets.
-    specialize  5Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
+    specialize Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
       intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ];
 	auto with sets.
     intros x1 H'4; try assumption.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 88cdabe3f..ec44a6e58 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -87,7 +87,7 @@ Section Integers_sect.
     apply Totally_ordered_definition.
     simpl in |- *.
     intros H' x y H'0.
-    specialize  2le_or_lt with (n := x) (m := y); intro H'2; elim H'2.
+    elim le_or_lt with (n := x) (m := y).
     intro H'1; left; auto with sets arith.
     intro H'1; right.
     cut (y <= x); auto with sets arith.
@@ -142,8 +142,8 @@ Section Integers_sect.
     elim H'0; intros H'1 H'2.
     cut (In nat Integers (S x)).
     intro H'3.
-    specialize  1H'2 with (y := S x); intro H'4; lapply H'4;
-      [ intro H'5; clear H'4 | try assumption; clear H'4 ].
+    specialize H'2 with (y := S x); lapply H'2;
+      [ intro H'5; clear H'2 | try assumption; clear H'2 ].
     simpl in H'5.
     absurd (S x <= x); auto with arith.
     apply triv_nat.
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index a7da7db9a..d5257c12c 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -140,10 +140,10 @@ intros U R H' x b H'0; elim H'0.
 intros x0 a H'1; exists a; auto with sets.
 intros x0 y z H'1 H'2 H'3 a H'4.
 red in H'.
-specialize  3H' with (x := x0) (a := a) (b := y); intro H'7; lapply H'7;
+specialize H' with (x := x0) (a := a) (b := y); lapply H'; 
  [ intro H'8; lapply H'8;
-    [ intro H'9; try exact H'9; clear H'8 H'7 | clear H'8 H'7 ]
- | clear H'7 ]; auto with sets.
+    [ intro H'9; try exact H'9; clear H'8 H' | clear H'8 H' ]
+ | clear H' ]; auto with sets.
 elim H'9.
 intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5.
 elim (H'3 t); auto with sets.