From 77e3f7be0533fad2c31eb302a51c74b829f99e8c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 8 Aug 2017 15:54:27 +0200
Subject: Introducing a syntax for goal dispatch.

---
 tests/tacticals.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'tests')

diff --git a/tests/tacticals.v b/tests/tacticals.v
index 73f9c03b87..1a2fbcbb37 100644
--- a/tests/tacticals.v
+++ b/tests/tacticals.v
@@ -20,3 +20,15 @@ first [
 | Message.print (Message.of_string "I won't be printed")
 ].
 Qed.
+
+Goal True /\ True.
+Proof.
+Fail split > [ split | |].
+split > [split | split].
+Qed.
+
+Goal True /\ (True -> True) /\ True.
+Proof.
+split > [ | split] > [split | .. | split].
+intros H; refine &H.
+Qed.
-- 
cgit v1.2.3