From 3fbba861d5355cad92cac52965c8e76a35825c7a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 8 Aug 2017 14:21:11 +0200
Subject: Another batch of primitive operations.

---
 tests/tacticals.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 tests/tacticals.v

(limited to 'tests')

diff --git a/tests/tacticals.v b/tests/tacticals.v
new file mode 100644
index 0000000000..73f9c03b87
--- /dev/null
+++ b/tests/tacticals.v
@@ -0,0 +1,22 @@
+Require Import Ltac2.Ltac2.
+
+Import Ltac2.Notations.
+
+Goal True.
+Proof.
+Fail fail.
+Fail solve [ () ].
+try fail.
+repeat fail.
+repeat ().
+solve [ constructor ].
+Qed.
+
+Goal True.
+Proof.
+first [
+  Message.print (Message.of_string "Yay"); fail
+| constructor
+| Message.print (Message.of_string "I won't be printed")
+].
+Qed.
-- 
cgit v1.2.3