diff options
| -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. |