From cc46417aad0bb80e3617baaf37fee93f1ea3034e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Jun 2008 19:36:10 +0000
Subject: - Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.
 - Test match dépendant.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11095 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Cases-bug1834.v | 13 +++++++++++++
 theories/Logic/EqdepFacts.v        | 19 ++++++-------------
 2 files changed, 19 insertions(+), 13 deletions(-)
 create mode 100644 test-suite/success/Cases-bug1834.v

diff --git a/test-suite/success/Cases-bug1834.v b/test-suite/success/Cases-bug1834.v
new file mode 100644
index 0000000000..543ca0c924
--- /dev/null
+++ b/test-suite/success/Cases-bug1834.v
@@ -0,0 +1,13 @@
+(* Bug in the computation of generalization *)
+
+(* The following bug, elaborated by Bruno Barras, is solved from r11083  *)
+
+Parameter P : unit -> Prop.
+Definition T := sig P.
+Parameter Q : T -> Prop.
+Definition U := sig Q.
+Parameter a : U.
+Check (match a with exist (exist tt e2) e3 => e3=e3 end).
+
+(* There is still a form submitted by Pierre Corbineau (#1834) which fails *)
+
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 7e02d06f33..b457a55b99 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -104,7 +104,7 @@ Implicit Arguments eq_dep1 [U P].
 
 (** Dependent equality is equivalent to equality on dependent pairs *)
 
-Lemma eq_sigS_eq_dep :
+Lemma eq_sigT_eq_dep :
   forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
     existT P p x = existT P q y -> eq_dep p x q y.
 Proof.
@@ -113,26 +113,19 @@ Proof.
   apply eq_dep_intro.
 Qed.
 
+Notation eq_sigS_eq_dep := eq_sigT_eq_dep (only parsing). (* Compatibility *)
+
 Lemma equiv_eqex_eqdep :
   forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
-   existS P p x = existS P q y <-> eq_dep p x q y.
+   existT P p x = existT P q y <-> eq_dep p x q y.
 Proof.
   split. 
   (* -> *)
-  apply eq_sigS_eq_dep.
+  apply eq_sigT_eq_dep.
   (* <- *)
   destruct 1; reflexivity.
 Qed.
 
-Lemma eq_sigT_eq_dep :
-  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
-    existT P p x = existT P q y -> eq_dep p x q y.
-Proof.
-  intros.
-  dependent rewrite H.
-  apply eq_dep_intro.
-Qed.
-
 Lemma eq_dep_eq_sigT :
   forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
     eq_dep p x q y -> existT P p x = existT P q y.
@@ -258,7 +251,7 @@ Section Corollaries.
  Proof.
    intro eq_dep_eq; red; intros.
    apply eq_dep_eq.
-   apply eq_sigS_eq_dep.
+   apply eq_sigT_eq_dep.
    assumption.
  Qed.
 
-- 
cgit v1.2.3