diff options
| author | Maxime Dénès | 2015-07-02 16:17:05 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-07-02 16:17:05 +0200 |
| commit | f59426dc74b86acebcda489f51453e036c3db451 (patch) | |
| tree | 98737ab611d42142c0d5c1a4efb75f5a42196618 | |
| parent | 27de0f2d7e5cd0cc4b221413dfe3c7b739104350 (diff) | |
Remove a line from test-suite.
Triggers a bug in declarative mode. Waiting for someone to volunteer and fix
the bug, but meanwhile I'm trying to fix the test-suite.
| -rw-r--r-- | test-suite/success/decl_mode2.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/success/decl_mode2.v b/test-suite/success/decl_mode2.v index 3ed622bf7f..46174e4810 100644 --- a/test-suite/success/decl_mode2.v +++ b/test-suite/success/decl_mode2.v @@ -123,10 +123,13 @@ Abort. Theorem T: forall (A:Prop) (P:nat -> Prop), P 2 -> A -> A /\ (forall x, x = 2 -> P x). intros A P HP HA. proof. +(* BUG: the next line fails when it should succeed. +Waiting for someone to investigate the bug. focus on (forall x, x = 2 -> P x). let x be such that (x = 2). hence thesis by HP. end focus. +*) Abort. Theorem T: forall x, x = 0 -> x + x = x * x. |