diff options
| author | Pierre-Marie Pédrot | 2017-10-30 15:53:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-30 17:12:16 +0100 |
| commit | a997ee7d78d90740b15b58502a1dc5e587b43ee3 (patch) | |
| tree | 0af87e2a77690deda29bec02a978076dd8f89d7e /tests/example2.v | |
| parent | f18502f32fb25b29cafe26340edbbcedd463c646 (diff) | |
Introducing the change tactic.
Diffstat (limited to 'tests/example2.v')
| -rw-r--r-- | tests/example2.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tests/example2.v b/tests/example2.v index 20819606db..46e4e43ed0 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -260,3 +260,9 @@ Proof. assert (H : 0 + 0 = 0) by reflexivity. intros x; exact x. Qed. + +Goal 1 + 1 = 2. +Proof. +change (?a + 1 = 2) with (2 = $a + 1). +reflexivity. +Qed. |