Remove "is_polymorphic_univ" checks in upper layers.

There were 2:

- when declaring a constraint to avoid monomorphic constraint
  referring to polymorphic univs, this check is redundant with the
  check in Section.ml

- when declaring a universe context to avoid redeclaring universes,
  this is not necessary after recent commits.

1 files changed, 5 insertions, 25 deletions

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 3ec6f884be..32447f31c1 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -52,11 +52,7 @@ let name_instance inst =
 
 let declare_universe_context ~poly ctx =
   if poly then
-    (* FIXME: some upper layers declare universes several times, we hack around
-      by checking whether the universes already exist. *)
-    let (univs, cstr) = ctx in
-    let univs = Univ.LSet.filter (fun u -> not (Lib.is_polymorphic_univ u)) univs in
-    let uctx = Univ.ContextSet.to_context (univs, cstr) in
+    let uctx = Univ.ContextSet.to_context ctx in
     let nas = name_instance (Univ.UContext.instance uctx) in
     Global.push_section_context (nas, uctx)
   else
@@ -606,28 +602,12 @@ let do_universe ~poly l =
 let do_constraint ~poly l =
   let open Univ in
   let u_of_id x =
-    let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
-    Lib.is_polymorphic_univ level, level
-  in
-  let in_section = Lib.sections_are_opened () in
-  let () =
-    if poly && not in_section then
-      CErrors.user_err ~hdr:"Constraint"
-                    (str"Cannot declare polymorphic constraints outside sections")
-  in
-  let check_poly p p' =
-    if poly then ()
-    else if p || p' then
-      CErrors.user_err ~hdr:"Constraint"
-                    (str "Cannot declare a global constraint on " ++
-                    str "a polymorphic universe, use "
-                    ++ str "Polymorphic Constraint instead")
+    Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x
   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 p p';
-     Constraint.add (lu, d, ru) acc)
-    Constraint.empty l
+      let lu = u_of_id l and ru = u_of_id r in
+      Constraint.add (lu, d, ru) acc)
+      Constraint.empty l
   in
   let uctx = ContextSet.add_constraints constraints ContextSet.empty in
   declare_universe_context ~poly uctx