From bc0cdb37c2117830f003a7fd8d87dbc12e4f085d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 6 Nov 2014 11:29:37 +0100 Subject: Removing "destruct" test not yet working. --- test-suite/success/destruct.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 8e9be2e40..e30f95ac3 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -317,7 +317,7 @@ destruct S'. Abort. (* This was working by chance in 8.4 thanks to "accidental" use of select - subterms _syntactically_ equal to the first matching one. *) + subterms _syntactically_ equal to the first matching one. Parameter f2:bool -> unit. Parameter r2:f2 true=f2 true. @@ -325,6 +325,7 @@ Goal forall (P: forall b, b=b -> Prop), f2 (id true) = tt -> P (f2 true) r2. intros. destruct f2. Abort. +*) (* This did not work in 8.4, because of a clear failing *) -- cgit v1.2.3