diff options
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 9ee312ff..a1c0c9ae 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_constr.ml4 8875 2006-05-29 19:59:11Z msozeau $ *) +(* $Id: g_constr.ml4 9043 2006-07-12 10:06:40Z herbelin $ *) open Pcoq open Constr @@ -244,6 +244,7 @@ GEXTEND Gram fixannot: [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec) | "{"; IDENT "wf"; id=name; rel=lconstr; "}" -> (Some id, CWfRec rel) + | "{"; IDENT "measure"; id=name; rel=lconstr; "}" -> (Some id, CMeasureRec rel) | -> (None, CStructRec) ] ] ; @@ -273,24 +274,25 @@ GEXTEND Gram [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ] ; eqn: - [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ] + [ [ pll = LIST0 LIST1 pattern LEVEL "99" SEP "," SEP "|"; + "=>"; rhs = lconstr -> (loc,pll,rhs) ] ] ; pattern: [ "200" RIGHTA [ ] - | "100" LEFTA + | "100" RIGHTA [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (loc,p::pl) ] | "99" RIGHTA [ ] | "10" LEFTA - [ p = pattern; lp = LIST1 (pattern LEVEL "0") -> + [ p = pattern; lp = LIST1 NEXT -> (match p with | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) | _ -> Util.user_err_loc (cases_pattern_loc p, "compound_pattern", Pp.str "Constructor expected")) | p = pattern; "as"; id = ident -> - CPatAlias (loc, p, id) - | c = pattern; "%"; key=IDENT -> - CPatDelimiters (loc,key,c) ] + CPatAlias (loc, p, id) ] + | "1" LEFTA + [ c = pattern; "%"; key=IDENT -> CPatDelimiters (loc,key,c) ] | "0" [ r = Prim.reference -> CPatAtom (loc,Some r) | "_" -> CPatAtom (loc,None) |