From 76adb57c72fccb4f3e416bd7f3927f4fff72178b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 1 Jun 2014 10:26:26 +0200
Subject: Making those proofs which depend on names generated for the arguments
 in Prop of constructors of inductive types independent of these names.

Incidentally upgraded/simplified a couple of proofs, mainly in Reals.

This prepares to the next commit about using names based on H for such
hypotheses in Prop.
---
 theories/Structures/DecidableTypeEx.v | 2 +-
 theories/Structures/EqualitiesFacts.v | 2 +-
 theories/Structures/OrderedType.v     | 8 ++++----
 theories/Structures/OrderedTypeEx.v   | 4 ++--
 4 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'theories/Structures')

diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v
index 971fcd7f8..163a40f2e 100644
--- a/theories/Structures/DecidableTypeEx.v
+++ b/theories/Structures/DecidableTypeEx.v
@@ -88,7 +88,7 @@ Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
  destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
  unfold eq, D1.eq, D2.eq in *; simpl;
  (left; f_equal; auto; fail) ||
- (right; intro H; injection H; auto).
+ (right; injection; auto).
  Defined.
 
 End PairUsualDecidableType.
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index c69885b46..11d94c119 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -166,7 +166,7 @@ Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
  destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
  unfold eq, D1.eq, D2.eq in *; simpl;
  (left; f_equal; auto; fail) ||
- (right; intro H; injection H; auto).
+ (right; intros [=]; auto).
  Defined.
 
 End PairUsualDecidableType.
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index fa08f9366..b9510342c 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -85,16 +85,16 @@ Module OrderedTypeFacts (Import O: OrderedType).
 
   Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
   Proof.
-   intros; destruct (compare x z); auto.
+   intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto.
    elim (lt_not_eq H); apply eq_trans with z; auto.
-   elim (lt_not_eq (lt_trans l H)); auto.
+   elim (lt_not_eq (lt_trans Hlt H)); auto.
   Qed.
 
   Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.
   Proof.
-   intros; destruct (compare x z); auto.
+   intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto.
    elim (lt_not_eq H0); apply eq_trans with x; auto.
-   elim (lt_not_eq (lt_trans H0 l)); auto.
+   elim (lt_not_eq (lt_trans H0 Hlt)); auto.
   Qed.
 
   Instance lt_compat : Proper (eq==>eq==>iff) lt.
diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
index 83130deb2..3c6afc7b2 100644
--- a/theories/Structures/OrderedTypeEx.v
+++ b/theories/Structures/OrderedTypeEx.v
@@ -279,7 +279,7 @@ Module PositiveOrderedTypeBits <: UsualOrderedType.
   Proof.
   induction x; destruct y.
   - (* I I *)
-    destruct (IHx y).
+    destruct (IHx y) as [l|e|g].
     apply LT; auto.
     apply EQ; rewrite e; red; auto.
     apply GT; auto.
@@ -290,7 +290,7 @@ Module PositiveOrderedTypeBits <: UsualOrderedType.
   - (* O I *)
     apply LT; simpl; auto.
   - (* O O *)
-    destruct (IHx y).
+    destruct (IHx y) as [l|e|g].
     apply LT; auto.
     apply EQ; rewrite e; red; auto.
     apply GT; auto.
-- 
cgit v1.2.3