diff options
| author | Pierre-Marie Pédrot | 2017-08-02 20:37:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-02 21:08:07 +0200 |
| commit | 9db02b3bfe35c15c9df8615f0e47a2a6407e858b (patch) | |
| tree | 3091b1da24a83270f57470e58cbdac0907019cd9 /tests/example2.v | |
| parent | 3007909ca1f65132bd0850d2be57e781e55707bd (diff) | |
Inserting enter functions in Ltac1 bindings.
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. |