diff options
| author | Matthieu Sozeau | 2014-07-01 22:50:37 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-01 22:52:08 +0200 |
| commit | 4c97e4ce19ca4c387039cfdcb4f24658100230b0 (patch) | |
| tree | 8e6367b1936d842b3e56283abc25de2342452884 /parsing | |
| parent | 3d2582eeb492fb21b7136016bf4c1a0463dc15c2 (diff) | |
Add toplevel commands to declare global universes and constraints.
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) ] ] |