diff options
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 23 |
1 files changed, 15 insertions, 8 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 7e5933cea..db68a75e0 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -155,9 +155,15 @@ GEXTEND Gram | "Type" -> Sorts.InType ] ] ; + universe_expr: + [ [ id = global; "+"; n = natural -> Some (id,n) + | id = global -> Some (id,0) + | "_" -> None + ] ] + ; universe: - [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids - | id = name -> [id] + [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> ids + | u = universe_expr -> [u] ] ] ; lconstr: @@ -261,17 +267,17 @@ GEXTEND Gram | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) + CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([[p]], c2)]) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) + CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([[p]], c2)]) | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) + CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([[p]], c2)]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> @@ -307,8 +313,9 @@ GEXTEND Gram universe_level: [ [ "Set" -> GSet | "Prop" -> GProp - | "Type" -> GType None - | id = name -> GType (Some id) + | "Type" -> GType UUnknown + | "_" -> GType UAnonymous + | id = global -> GType (UNamed id) ] ] ; fix_constr: @@ -355,7 +362,7 @@ GEXTEND Gram [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ] ; mult_pattern: - [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (Loc.tag ~loc:!@loc pl) ] ] + [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> pl ] ] ; eqn: [ [ pll = LIST1 mult_pattern SEP "|"; |