From a997ee7d78d90740b15b58502a1dc5e587b43ee3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 30 Oct 2017 15:53:55 +0100
Subject: Introducing the change tactic.

---
 tests/example2.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'tests')

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.
-- 
cgit v1.2.3