diff options
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/g_constr.ml4 | 6 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 4 | ||||
-rw-r--r-- | parsing/pcoq.ml | 1 | ||||
-rw-r--r-- | parsing/pcoq.mli | 1 |
4 files changed, 7 insertions, 5 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 74994c5e3..7f3a3d10c 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -127,7 +127,7 @@ let name_colon = let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None GEXTEND Gram - GLOBAL: binder_constr lconstr constr operconstr sort global + GLOBAL: binder_constr lconstr constr operconstr universe_level sort global constr_pattern lconstr_pattern Constr.ident closed_binder open_binders binder binders binders_fixannot record_declaration typeclass_constraint pattern appl_arg; @@ -298,10 +298,10 @@ GEXTEND Gram | -> [] ] ] ; instance: - [ [ "@{"; l = LIST1 level; "}" -> Some l + [ [ "@{"; l = LIST1 universe_level; "}" -> Some l | -> None ] ] ; - level: + universe_level: [ [ "Set" -> GSet | "Prop" -> GProp | "Type" -> GType None diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 1a4012891..50e469dd2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -226,8 +226,8 @@ GEXTEND Gram [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ] ; univ_constraint: - [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; - r = identref -> (l, ord, r) ] ] + [ [ l = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; + r = universe_level -> (l, ord, r) ] ] ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 714e25f85..4e069c9e3 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -304,6 +304,7 @@ module Constr = let binder_constr = gec_constr "binder_constr" let ident = make_gen_entry uconstr "ident" let global = make_gen_entry uconstr "global" + let universe_level = make_gen_entry uconstr "universe_level" let sort = make_gen_entry uconstr "sort" let pattern = Gram.entry_create "constr:pattern" let constr_pattern = gec_constr "constr_pattern" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 635b0170a..7f49c997f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -157,6 +157,7 @@ module Constr : val operconstr : constr_expr Gram.entry val ident : Id.t Gram.entry val global : reference Gram.entry + val universe_level : glob_level Gram.entry val sort : glob_sort Gram.entry val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry |