aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-09-29 15:51:18 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-09-29 15:56:10 +0200
commit9615c025a2a09b69f2001d44a66a1fddef74e680 (patch)
tree4643d4f0f38b89402265df46c56119e28a8afe40 /parsing
parent5348a615a484e379896deac8a6944af1f92b2d4c (diff)
Fix bug #4869, allow Prop, Set, and level names in constraints.
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_constr.ml46
-rw-r--r--parsing/g_vernac.ml44
-rw-r--r--parsing/pcoq.ml1
-rw-r--r--parsing/pcoq.mli1
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 c09693b36..78176d934 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