[declare] Split universe declaration code to vernac/

The code is self-contained and only used by commands; this also
highlights the several `Libobject.obj` registered for each
declaration.

2 files changed, 2 insertions, 111 deletions

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 7d32f1a7e8..412f735983 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -538,106 +538,3 @@ let assumption_message id =
   the type of the object than to the name of the object (see
   discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
   Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
-
-(** Global universes are not substitutive objects but global objects
-   bound at the *library* or *module* level. The polymorphic flag is
-   used to distinguish universes declared in polymorphic sections, which
-   are discharged and do not remain in scope. *)
-
-type universe_source =
-  | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *)
-  | QualifiedUniv of Id.t (* global universe introduced by some global value *)
-  | UnqualifiedUniv (* other global universe *)
-
-type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list
-
-let check_exists_universe sp =
-  if Nametab.exists_universe sp then
-    raise (AlreadyDeclared (Some "Universe", Libnames.basename sp))
-  else ()
-
-let qualify_univ i dp src id =
-  match src with
-  | BoundUniv | UnqualifiedUniv ->
-    i,  Libnames.make_path dp id
-  | QualifiedUniv l ->
-    let dp = DirPath.repr dp in
-    Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id
-
-let do_univ_name ~check i dp src (id,univ) =
-  let i, sp = qualify_univ i dp src id in
-  if check then check_exists_universe sp;
-  Nametab.push_universe i sp univ
-
-let cache_univ_names ((sp, _), (src, univs)) =
-  let depth = sections_depth () in
-  let dp = Libnames.pop_dirpath_n depth (Libnames.dirpath sp) in
-  List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs
-
-let load_univ_names i ((sp, _), (src, univs)) =
-  List.iter (do_univ_name ~check:false (Nametab.Until i) (Libnames.dirpath sp) src) univs
-
-let open_univ_names i ((sp, _), (src, univs)) =
-  List.iter (do_univ_name ~check:false (Nametab.Exactly i) (Libnames.dirpath sp) src) univs
-
-let discharge_univ_names = function
-  | _, (BoundUniv, _) -> None
-  | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x
-
-let input_univ_names : universe_name_decl -> Libobject.obj =
-  declare_object
-    { (default_object "Global universe name state") with
-      cache_function = cache_univ_names;
-      load_function = load_univ_names;
-      open_function = open_univ_names;
-      discharge_function = discharge_univ_names;
-      subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
-      classify_function = (fun a -> Substitute a) }
-
-let declare_univ_binders gr pl =
-  if Global.is_polymorphic gr then
-    ()
-  else
-    let l = let open GlobRef in match gr with
-      | ConstRef c -> Label.to_id @@ Constant.label c
-      | IndRef (c, _) -> Label.to_id @@ MutInd.label c
-      | VarRef id ->
-        CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
-      | ConstructRef _ ->
-        CErrors.anomaly ~label:"declare_univ_binders"
-          Pp.(str "declare_univ_binders on an constructor reference")
-    in
-    let univs = Id.Map.fold (fun id univ univs ->
-        match Univ.Level.name univ with
-        | None -> assert false (* having Prop/Set/Var as binders is nonsense *)
-        | Some univ -> (id,univ)::univs) pl []
-    in
-    Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
-
-let do_universe ~poly l =
-  let in_section = Global.sections_are_opened () in
-  let () =
-    if poly && not in_section then
-      CErrors.user_err ~hdr:"Constraint"
-                   (str"Cannot declare polymorphic universes outside sections")
-  in
-  let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in
-  let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
-      Univ.LSet.empty l, Univ.Constraint.empty
-  in
-  let src = if poly then BoundUniv else UnqualifiedUniv in
-  let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
-  declare_universe_context ~poly ctx
-
-let do_constraint ~poly l =
-  let open Univ in
-  let u_of_id x =
-    Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x
-  in
-  let constraints = List.fold_left (fun acc (l, d, r) ->
-      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 a6c1374a77..bf5877d4c4 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -43,6 +43,8 @@ type 'a constant_entry =
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
+
 val declare_variable
   :  name:variable
   -> kind:Decls.logical_kind
@@ -102,13 +104,5 @@ val recursive_message : bool (** true = fixpoint *) ->
 
 val exists_name : Id.t -> bool
 
-(** Global universe contexts, names and constraints *)
-val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
-
-val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
-
-val do_universe : poly:bool -> lident list -> unit
-val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit
-
 (* Used outside this module only in indschemes *)
 exception AlreadyDeclared of (string option * Id.t)