diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 39c93e316c..5f49a318d4 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -210,6 +210,8 @@ GEXTEND Gram l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) | IDENT "Register"; IDENT "Inline"; id = identref -> VernacRegister(id, RegisterInline) + | IDENT "Universe"; l = LIST1 identref -> VernacUniverse l + | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> VernacConstraint l ] ] ; @@ -256,6 +258,10 @@ GEXTEND Gram | IDENT "Inline" -> DefaultInline | -> NoInline] ] ; + univ_constraint: + [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; + r = identref -> (l, ord, r) ] ] + ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) | "CoInductive" -> (CoInductive,CoFinite) ] ] |