diff options
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index f637e9746..7d0728458 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -123,8 +123,8 @@ let name_colon = let aliasvar = function { CAst.loc = loc; CAst.v = CPatAlias (_, id) } -> Some (loc,Name id) | _ -> None GEXTEND Gram - GLOBAL: binder_constr lconstr constr operconstr universe_level sort global - constr_pattern lconstr_pattern Constr.ident + GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family + global constr_pattern lconstr_pattern Constr.ident closed_binder open_binders binder binders binders_fixannot record_declaration typeclass_constraint pattern appl_arg; Constr.ident: @@ -149,6 +149,12 @@ GEXTEND Gram | "Type"; "@{"; u = universe; "}" -> GType u ] ] ; + sort_family: + [ [ "Set" -> Sorts.InSet + | "Prop" -> Sorts.InProp + | "Type" -> Sorts.InType + ] ] + ; universe: [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids | id = name -> [id] |