diff options
| author | herbelin | 2003-04-29 12:02:34 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-29 12:02:34 +0000 |
| commit | a4ebbd6dffcf6182c4b7a218ce90c1c8f0254daa (patch) | |
| tree | 6a65d469dd5702267b855da16ed05bdca6ddfc85 /parsing/g_constrnew.ml4 | |
| parent | 4b9070eefcdb135226fb4f3c2706519796b0284e (diff) | |
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
Diffstat (limited to 'parsing/g_constrnew.ml4')
| -rw-r--r-- | parsing/g_constrnew.ml4 | 11 |
1 files changed, 7 insertions, 4 deletions
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) ] ] |