From a4ebbd6dffcf6182c4b7a218ce90c1c8f0254daa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 Apr 2003 12:02:34 +0000
Subject: Factorisation des produits de même type; parenthèses autour des x:=c
 et n:=c dans les 'with bindings'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3974 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_constrnew.ml4 | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'parsing/g_constrnew.ml4')

diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index ba8be907cf..ffc7d403c5 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -153,7 +153,7 @@ GEXTEND Gram
       | "("; c=operconstr; ")" -> c ] ]
   ;
   binder_constr:
-    [ [ "!"; bl = LIST1 binder; "."; c = operconstr LEVEL "200" ->
+    [ [ "!"; bl = binder_list; "."; c = operconstr LEVEL "200" ->
           CProdN(loc,bl,c)
       | "fun"; bl = LIST1 binder; ty = type_cstr; "=>";
         c = operconstr LEVEL "200" ->
@@ -244,11 +244,14 @@ GEXTEND Gram
     [ [ c = pattern -> c
       | p1=pattern; ","; p2=lpattern ->  CPatCstr (loc, pair loc, [p1;p2]) ] ]
   ;
+  binder_list:
+    [ [ idl=LIST1 name; bl=LIST0 binder -> (idl,CHole loc)::bl
+      | "("; idl=LIST1 name; ":"; c=lconstr; ")"; bl=LIST0 binder ->(idl,c)::bl
+      | idl=LIST1 name; ":"; c=constr -> [(idl,c)] ] ]
+  ;
   binder:
     [ [ id=name -> ([id],CHole loc)
-      | "("; id=name; ")" -> ([id],CHole loc)
-      | "("; id=name; ":"; c=lconstr; ")" -> ([id],c)
-      | id=name; ":"; c=constr -> ([id],c) ] ] (* tolerance *)
+      | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,c) ] ]
   ;
   type_cstr:
     [ [ c=OPT [":"; c=lconstr -> c] -> (loc,c) ] ]
-- 
cgit v1.2.3