From 5350d21315f6c6347c0b44e510ed8b8805cc2119 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 10 Sep 2014 10:18:24 +0200 Subject: 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. --- test-suite/success/Inversion.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'test-suite/success') 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. -- cgit v1.2.3