Merge PR #8100: Use just one object declaration for all global universe additions

2 files changed, 7 insertions, 39 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 0222aeb283..532339c03c 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -597,27 +597,8 @@ let do_universe poly l =
       ignore(Lib.add_leaf id (input_universe (src, lev))))
     l
 
-type constraint_decl = polymorphic * Univ.Constraint.t
-
-let cache_constraints (na, (p, c)) =
-  let ctx =
-    Univ.ContextSet.add_constraints c
-      Univ.ContextSet.empty (* No declared universes here, just constraints *)
-  in cache_universe_context (p,ctx)
-
-let discharge_constraints (_, (p, c as a)) =
-  if p then None else Some a
-
-let input_constraints : constraint_decl -> Libobject.obj =
-  let open Libobject in
-    declare_object
-    { (default_object "Global universe constraints") with
-      cache_function = cache_constraints;
-      load_function = (fun _ -> cache_constraints);
-      discharge_function = discharge_constraints;
-      classify_function = (fun a -> Keep a) }
-
 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
     UnivNames.is_polymorphic level, level
@@ -639,7 +620,8 @@ let do_constraint poly l =
   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';
-     Univ.Constraint.add (lu, d, ru) acc)
-    Univ.Constraint.empty l
+     Constraint.add (lu, d, ru) acc)
+    Constraint.empty l
   in
-    Lib.add_anonymous_leaf (input_constraints (poly, constraints))
+  let uctx = ContextSet.add_constraints constraints ContextSet.empty in
+  declare_universe_context poly uctx
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 09b2e59cea..43a450ea71 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -886,20 +886,6 @@ let pr_hint_term env sigma ctx = function
      let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
      pr_econstr_env env sigma c
 
-(** We need an object to record the side-effect of registering
-  global universes associated with a hint. *)
-let cache_context_set (_,c) =
-  Global.push_context_set false c
-
-let input_context_set : Univ.ContextSet.t -> Libobject.obj =
-  let open Libobject in
-    declare_object
-    { (default_object "Global universe context") with
-      cache_function = cache_context_set;
-      load_function = (fun _ -> cache_context_set);
-      discharge_function = (fun (_,a) -> Some a);
-      classify_function = (fun a -> Keep a) }
-
 let warn_polymorphic_hint =
   CWarnings.create ~name:"polymorphic-hint" ~category:"automation"
          (fun hint -> strbrk"Using polymorphic hint " ++ hint ++
@@ -919,7 +905,7 @@ let fresh_global_or_constr env sigma poly cr =
     else begin
       if isgr then
         warn_polymorphic_hint (pr_hint_term env sigma ctx cr);
-      Lib.add_anonymous_leaf (input_context_set ctx);
+      Declare.declare_universe_context false ctx;
       (c, Univ.ContextSet.empty)
     end
 
@@ -1315,7 +1301,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
     else if local then IsConstr (c', diff)
-    else (Lib.add_anonymous_leaf (input_context_set diff);
+    else (Declare.declare_universe_context false diff;
 	  IsConstr (c', Univ.ContextSet.empty))
 
 let project_hint ~poly pri l2r r =