From d3eb7c916077eba740d9f35b6ac10358eb0fe934 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 6 Jul 2007 13:29:54 +0000
Subject: Suggestion of additional syntax for intro patterns:   intros
 {A,B,C,D} means:   intros (A,(B,(C,D)))

Should be especially useful when breaking existential hypthesis like 
 {n:nat | P n /\ Q n /\ R n }, hence the notation {}. 



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9948 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_tactic.ml4 | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 34cdd44d67..a15a6c12df 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -179,6 +179,12 @@ GEXTEND Gram
     [ [ "["; tc = LIST1 intropatterns SEP "|" ; "]" -> IntroOrAndPattern tc
       | "("; tc = LIST0 simple_intropattern SEP "," ; ")" -> IntroOrAndPattern [tc]
       | "()" -> IntroOrAndPattern [[]]
+      | "{"; tc = LIST0 simple_intropattern SEP "," ; "}" -> 
+	  (* {A,B,C} is translated into (A,(B,C)) *)
+	  let rec pairify = function 
+	    | ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l]
+	    | t::q -> IntroOrAndPattern [[t;pairify q]]
+	  in pairify tc
       | "_" -> IntroWildcard
       | "?" -> IntroAnonymous
       | id = ident -> IntroIdentifier id
-- 
cgit v1.2.3