aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml24
-rw-r--r--library/declare.mli4
2 files changed, 19 insertions, 9 deletions
diff --git a/library/declare.ml b/library/declare.ml
index 3d063225f..7025839d0 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 7824506da..4051174a7 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