diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-06 11:29:37 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-06 12:05:48 +0100 |
| commit | bc0cdb37c2117830f003a7fd8d87dbc12e4f085d (patch) | |
| tree | 504a99972483155319d62065c6da6aed0e61849e | |
| parent | 6ae459fe810a1907a0afcfe9ecf5c062cae60f17 (diff) | |
Removing "destruct" test not yet working.
| -rw-r--r-- | test-suite/success/destruct.v | 3 |
1 files changed, 2 insertions, 1 deletions
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 *) |