diff options
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. |