diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 12:51:16 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 12:51:16 +0200 |
| commit | 7543449792d417a92092b692986d62b622b78ffc (patch) | |
| tree | 8244b6c3efa88abe12ab990a4ae4b3d0af8f5dc1 /parsing | |
| parent | bff880ffb6ef33c99a96e7925c995b31b1497e6a (diff) | |
| parent | 9615c025a2a09b69f2001d44a66a1fddef74e680 (diff) | |
Merge remote-tracking branch 'github/pr/299' into v8.6
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in
constraints.
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 |