Merge PR #10670: ComAssumption cleanup

Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot

2 files changed, 11 insertions, 33 deletions

diff --git a/tactics/declare.ml b/tactics/declare.ml
index b24a97e2d4..3590146dfb 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
@@ -302,7 +298,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
 (** Declaration of section variables and local definitions *)
 type variable_declaration =
   | SectionLocalDef of Evd.side_effects proof_entry
-  | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
+  | SectionLocalAssum of { typ:Constr.types; impl:Glob_term.binding_kind; }
 
 (* This object is only for things which iterate over objects to find
    variables (only Prettyp.print_context AFAICT) *)
@@ -315,11 +311,10 @@ let declare_variable ~name ~kind d =
   if Decls.variable_exists name then
     raise (AlreadyDeclared (None, name));
 
-  let impl,opaque,poly = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum {typ;univs;poly;impl} ->
-      let () = declare_universe_context ~poly univs in
+  let impl,opaque = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum {typ;impl} ->
       let () = Global.push_named_assum (name,typ) in
-      impl, true, poly
+      impl, true
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
@@ -342,8 +337,7 @@ let declare_variable ~name ~kind d =
         secdef_type = de.proof_entry_type;
       } in
       let () = Global.push_named_def (name, se) in
-      Glob_term.Explicit, de.proof_entry_opaque,
-      poly
+      Glob_term.Explicit, de.proof_entry_opaque
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
   Decls.(add_variable_data name {opaque;kind});
@@ -608,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
diff --git a/tactics/declare.mli b/tactics/declare.mli
index da66a2713c..f4bfdb1547 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -36,7 +36,7 @@ type 'a proof_entry = {
 
 type variable_declaration =
   | SectionLocalDef of Evd.side_effects proof_entry
-  | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
+  | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; }
 
 type 'a constant_entry =
   | DefinitionEntry of 'a proof_entry