diff options
Diffstat (limited to 'tests/example2.v')
| -rw-r--r-- | tests/example2.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/tests/example2.v b/tests/example2.v index fd5a9044e9..79f230ab57 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -23,6 +23,13 @@ Qed. Goal (forall n : nat, n = 0 -> False) -> True. Proof. intros H. +eelim &H. +split. +Qed. + +Goal (forall n : nat, n = 0 -> False) -> True. +Proof. +intros H. elim &H with 0. split. Qed. @@ -41,3 +48,16 @@ intros P H. eapply &H. split. Qed. + +Goal exists n, n = 0. +Proof. +Fail constructor 1. +constructor 1 with (x := 0). +split. +Qed. + +Goal exists n, n = 0. +Proof. +econstructor 1. +split. +Qed. |