diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ltac2/example2.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/ltac2/example2.v b/test-suite/ltac2/example2.v index c953d25061..ac92ca34ef 100644 --- a/test-suite/ltac2/example2.v +++ b/test-suite/ltac2/example2.v @@ -261,6 +261,25 @@ assert (H : 0 + 0 = 0) by reflexivity. intros x; exact x. Qed. +Goal True. +Proof. +enough (H := 0 + 0). +constructor. +Qed. + +Goal True. +Proof. +enough (exists n, n = 0) as [n Hn]. ++ exact I. ++ exists 0; reflexivity. +Qed. + +Goal True -> True. +Proof. +enough (H : 0 + 0 = 0) by (intros x; exact x). +reflexivity. +Qed. + Goal 1 + 1 = 2. Proof. change (?a + 1 = 2) with (2 = $a + 1). |