From f99dc2691ace6a691e7fd07e580e855e7bca7b55 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 27 Sep 2009 07:56:55 +0000
Subject: Delay the choice of eliminator in destruct/induction until we know if
 a dependent scheme is needed or not (this allows for instance "destruct H"
 when H is propositional and dependent in the context to work).

Modest attempt to clarify the basic components used and invariants
preserved when sharing the code for functional induction and for
destruct/induction.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12356 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/destruct.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index e5f1c61873..fb2c84c95f 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -61,3 +61,16 @@ End Properties.
 Goal forall P:(forall n, 0=n -> Prop), forall H: 0=0, P 0 H.
 destruct H.
 Abort.
+
+(* The calls to "destruct" below did not work before revision 12356 *)
+
+Variable A:Type.
+Variable P:A->Type.
+Require Import JMeq.
+Goal forall a b (p:P a) (q:P b), 
+  forall H:a = b, eq_rect a P p b H = q -> JMeq (existT _ a p) (existT _ b q).
+intros.
+destruct H.
+destruct H0.
+reflexivity.
+Qed.
-- 
cgit v1.2.3