diff options
| author | herbelin | 2009-09-27 07:56:55 +0000 |
|---|---|---|
| committer | herbelin | 2009-09-27 07:56:55 +0000 |
| commit | f99dc2691ace6a691e7fd07e580e855e7bca7b55 (patch) | |
| tree | 3ae1ac05155169ea776d573e7ee4ce5a42f592eb /test-suite | |
| parent | b7a2a4728aae75eba4750b7c3e0dc60c624b76cf (diff) | |
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
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/destruct.v | 13 |
1 files changed, 13 insertions, 0 deletions
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. |