aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.mli2
-rw-r--r--library/declare.ml24
-rw-r--r--library/declare.mli4
-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
-rw-r--r--printing/ppconstr.ml6
-rw-r--r--printing/ppconstrsig.mli1
-rw-r--r--printing/ppvernac.ml3
-rw-r--r--test-suite/bugs/closed/4869.v18
-rw-r--r--toplevel/command.mli2
12 files changed, 55 insertions, 17 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ed44704df4..e6599a30d1 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -346,7 +346,7 @@ type vernac_expr =
| VernacScheme of (lident option * scheme) list
| VernacCombinedScheme of lident * lident list
| VernacUniverse of lident list
- | VernacConstraint of (lident * Univ.constraint_type * lident) list
+ | VernacConstraint of (glob_level * Univ.constraint_type * glob_level) list
(* Gallina extensions *)
| VernacBeginSection of lident
diff --git a/library/declare.ml b/library/declare.ml
index 3d063225f4..7025839d0c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -491,12 +491,20 @@ let input_constraints : constraint_decl -> Libobject.obj =
classify_function = (fun a -> Keep a) }
let do_constraint poly l =
- let u_of_id =
- let names, _ = Universes.global_universe_names () in
- fun (loc, id) ->
- try Idmap.find id names
- with Not_found ->
- user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+ let open Misctypes in
+ let u_of_id x =
+ match x with
+ | GProp -> Loc.dummy_loc, (false, Univ.Level.prop)
+ | GSet -> Loc.dummy_loc, (false, Univ.Level.set)
+ | GType None ->
+ user_err_loc (Loc.dummy_loc, "Constraint",
+ str "Cannot declare constraints on anonymous universes")
+ | GType (Some (loc, id)) ->
+ let id = Id.of_string id in
+ let names, _ = Universes.global_universe_names () in
+ try loc, Idmap.find id names
+ with Not_found ->
+ user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
in
let in_section = Lib.sections_are_opened () in
let () =
@@ -514,8 +522,8 @@ let do_constraint poly l =
++ str "Polymorphic Constraint instead")
in
let constraints = List.fold_left (fun acc (l, d, r) ->
- let p, lu = u_of_id l and p', ru = u_of_id r in
- check_poly (fst l) p (fst r) p';
+ let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in
+ check_poly ploc p rloc p';
Univ.Constraint.add (lu, d, ru) acc)
Univ.Constraint.empty l
in
diff --git a/library/declare.mli b/library/declare.mli
index 7824506da0..4051174a75 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -90,4 +90,6 @@ val exists_name : Id.t -> bool
(** Global universe names and constraints *)
val do_universe : polymorphic -> Id.t Loc.located list -> unit
-val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
+val do_constraint : polymorphic ->
+ (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
+ unit
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 74994c5e3d..7f3a3d10ca 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 c09693b364..78176d9346 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 714e25f85e..4e069c9e33 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 635b0170ae..7f49c997fe 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
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index a00e4bab30..aa0ebbb83b 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -149,6 +149,12 @@ end) = struct
| GType [] -> tag_type (str "Type")
| GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
+ let pr_glob_level = function
+ | GProp -> tag_type (str "Prop")
+ | GSet -> tag_type (str "Set")
+ | GType None -> tag_type (str "Type")
+ | GType (Some (_, u)) -> tag_type (str u)
+
let pr_qualid sp =
let (sl, id) = repr_qualid sp in
let id = tag_ref (pr_id id) in
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
index a59fc6d67d..3de0d805c4 100644
--- a/printing/ppconstrsig.mli
+++ b/printing/ppconstrsig.mli
@@ -44,6 +44,7 @@ module type Pp = sig
val pr_qualid : qualid -> std_ppcmds
val pr_patvar : patvar -> std_ppcmds
+ val pr_glob_level : glob_level -> std_ppcmds
val pr_glob_sort : glob_sort -> std_ppcmds
val pr_guard_annot : (constr_expr -> std_ppcmds) ->
local_binder list ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 40ce28dc0c..2c41d1146c 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -838,7 +838,8 @@ module Make
)
| VernacConstraint v ->
let pr_uconstraint (l, d, r) =
- pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r
+ pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
+ pr_glob_level r
in
return (
hov 2 (keyword "Constraint" ++ spc () ++
diff --git a/test-suite/bugs/closed/4869.v b/test-suite/bugs/closed/4869.v
new file mode 100644
index 0000000000..6d21b66fe9
--- /dev/null
+++ b/test-suite/bugs/closed/4869.v
@@ -0,0 +1,18 @@
+Universes i.
+
+Fail Constraint i < Set.
+Fail Constraint i <= Set.
+Fail Constraint i = Set.
+Constraint Set <= i.
+Constraint Set < i.
+Fail Constraint i < j. (* undeclared j *)
+Fail Constraint i < Type. (* anonymous *)
+
+Set Universe Polymorphism.
+
+Section Foo.
+ Universe j.
+ Constraint Set < j.
+
+ Definition foo := Type@{j}.
+End Foo. \ No newline at end of file
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d353724294..616afb91f0 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -22,7 +22,7 @@ open Pfedit
val do_universe : polymorphic -> Id.t Loc.located list -> unit
val do_constraint : polymorphic ->
- (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
+ (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> unit
(** {6 Hooks for Pcoq} *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:29:40 +0000