Fix bug #2695: infinite loop in dependent destruction.

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

1 files changed, 7 insertions, 3 deletions

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index d408845e7..dae967584 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -290,12 +290,14 @@ Lemma simplification_heq A B (x y : A) :
   (x = y -> B) -> (JMeq x y -> B).
 Proof. intros H J; apply H; apply (JMeq_eq J). Defined.
 
+Definition conditional_eq {A} (x y : A) := eq x y.
+
 Lemma simplification_existT2 A (P : A -> Type) B (p : A) (x y : P p) :
-  (x = y -> B) -> (existT P p x = existT P p y -> B).
+  (x = y -> B) -> (conditional_eq (existT P p x) (existT P p y) -> B).
 Proof. intros H E. apply H. apply inj_pair2. assumption. Defined.
 
 Lemma simplification_existT1 A (P : A -> Type) B (p q : A) (x : P p) (y : P q) :
-  (p = q -> existT P p x = existT P q y -> B) -> (existT P p x = existT P q y -> B).
+  (p = q -> conditional_eq (existT P p x) (existT P q y) -> B) -> (existT P p x = existT P q y -> B).
 Proof. injection 2. auto. Defined.
 
 Lemma simplification_K A (x : A) (B : x = x -> Type) :
@@ -319,8 +321,10 @@ Ltac simplify_one_dep_elim_term c :=
     | @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _)
     | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _)
     | eq (existT _ _ _) (existT _ _ _) -> _ =>
-      refine (simplification_existT2 _ _ _ _ _ _ _) ||
         refine (simplification_existT1 _ _ _ _ _ _ _ _)
+    | conditional_eq (existT _ _ _) (existT _ _ _) -> _ =>
+        refine (simplification_existT2 _ _ _ _ _ _ _) ||
+               (unfold conditional_eq; intro)
     | ?x = ?y -> _ => (* variables case *)
       (unfold x) || (unfold y) ||
       (let hyp := fresh in intros hyp ;