Fix bug #4869, allow Prop, Set, and level names in constraints.

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