diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-10 10:18:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-10 10:58:06 +0200 |
| commit | 5350d21315f6c6347c0b44e510ed8b8805cc2119 (patch) | |
| tree | b04c2d460d5a21e47bc0843a6244a1a989c54926 /test-suite/success | |
| parent | b3a5450370b64ef59bd08f9ac2dc3862b9a37e6c (diff) | |
Fixing inversion after having fixed intros_replacing
in69665dd2480d364162933972de7ffa955eccab4d. There are still situations
when "as" is not given where equations coming from injection are not
yet removed, making invalid the computation of dependencies, what
prevents an hypothesis to be cleared and replaced.
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/Inversion.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index b068f7298..892dd6d48 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -136,3 +136,23 @@ Goal True -> True. intro. Fail inversion H using False. Fail inversion foo using True_ind. + +(* Was failing at some time between 7 and 10 September 2014 *) +(* even though, it is not clear that the resulting context is interesting *) + +Parameter P:nat*nat->Prop. +Inductive IND : nat * nat -> { x : nat * nat | P x } * nat -> Prop := +CONSTR a b (H:P (a,b)) c : IND (a,b) (exist _ (a,b) H, c). + +Goal forall x y z t u (H':P (z,t)), IND (x,y) (exist _ (z,t) H', u) -> x = z. +intros * Hyp. +inversion Hyp. + (* By the way, why is "H" removed even in non-clear mode ? *) +reflexivity. +Qed. + +Goal forall x y z t u (H':P (z,t)), IND (x,y) (exist _ (z,t) H', u) -> x = z. +intros * Hyp. +inversion Hyp as (a,b,H,c,(H1_1,H1_2),(H2_1,H2_2,H2_3)). +reflexivity. +Qed. |