diff options
| author | Pierre-Marie Pédrot | 2017-11-02 11:41:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-11-02 11:52:17 +0100 |
| commit | 62606e17ff4afe6a897607d45471b7f4d3ef54b8 (patch) | |
| tree | 972102473076ef38585c909444a266f780b95a80 /tests/example2.v | |
| parent | de7483beb78e5bd81dc6449ba201fb9dfc490ba8 (diff) | |
Binding the specialize tactic.
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. |