diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/decl_mode2.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/decl_mode2.v b/test-suite/success/decl_mode2.v index 4475b5d479..edee439f00 100644 --- a/test-suite/success/decl_mode2.v +++ b/test-suite/success/decl_mode2.v @@ -81,7 +81,7 @@ Abort. Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B. intros A B C HA HB HC. proof. -hence C. (* fails *) +Fail hence C. (* fails *) Abort. Theorem T: forall (A B:Prop), B -> A \/ B. |