diff options
Diffstat (limited to 'tests/example2.v')
| -rw-r--r-- | tests/example2.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/tests/example2.v b/tests/example2.v index 46e4e43ed0..c953d25061 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -266,3 +266,16 @@ Proof. change (?a + 1 = 2) with (2 = $a + 1). reflexivity. Qed. + +Goal (forall n, n = 0 -> False) -> False. +Proof. +intros H. +specialize (H 0 eq_refl). +destruct H. +Qed. + +Goal (forall n, n = 0 -> False) -> False. +Proof. +intros H. +specialize (H 0 eq_refl) as []. +Qed. |