Split off Universes functions dealing with names.

This API is a bit strange, I expect it will change at some point.

5 files changed, 12 insertions, 12 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 185b1648c..d036fec21 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -35,8 +35,8 @@ open Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 type object_pr = {
-  print_inductive           : MutInd.t -> Universes.univ_name_list option -> Pp.t;
-  print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
+  print_inductive           : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+  print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
   print_section_variable    : env -> Evd.evar_map -> variable -> Pp.t;
   print_syntactic_def       : env -> KerName.t -> Pp.t;
   print_module              : bool -> ModPath.t -> Pp.t;
@@ -93,7 +93,7 @@ let print_ref reduce ref udecl =
   let inst = Univ.AUContext.instance univs in
   let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
   let env = Global.env () in
-  let bl = Universes.universe_binders_with_opt_names ref
+  let bl = UnivNames.universe_binders_with_opt_names ref
       (Array.to_list (Univ.Instance.to_array inst)) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let inst =
@@ -594,7 +594,7 @@ let print_constant with_values sep sp udecl =
   in
   let ctx =
     UState.of_binders
-      (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
+      (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
   let pr_ltype = pr_ltype_env env sigma in
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 2f2dcd563..50042d6c5 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -34,10 +34,10 @@ val print_eval :
     Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 
 val print_name : env -> Evd.evar_map -> reference or_by_notation ->
-  Universes.univ_name_list option -> Pp.t
+  UnivNames.univ_name_list option -> Pp.t
 val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
 val print_about : env -> Evd.evar_map -> reference or_by_notation ->
-  Universes.univ_name_list option -> Pp.t
+  UnivNames.univ_name_list option -> Pp.t
 val print_impargs : reference or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
@@ -84,8 +84,8 @@ val print_located_module : reference -> Pp.t
 val print_located_other : string -> reference -> Pp.t
 
 type object_pr = {
-  print_inductive           : MutInd.t -> Universes.univ_name_list option -> Pp.t;
-  print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
+  print_inductive           : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+  print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
   print_section_variable    : env -> Evd.evar_map -> variable -> Pp.t;
   print_syntactic_def       : env -> KerName.t -> Pp.t;
   print_module              : bool -> ModPath.t -> Pp.t;
diff --git a/printing/printer.ml b/printing/printer.ml
index edcce874d..77466605a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -293,7 +293,7 @@ let pr_global = pr_global_env Id.Set.empty
 let pr_puniverses f env (c,u) =
   f env c ++ 
   (if !Constrextern.print_universes then
-    str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+    str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
    else mt ())
 
 let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index e076c10f3..3c805b327 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -140,7 +140,7 @@ let print_mutual_inductive env mind mib udecl =
                        (AUContext.instance (Declareops.inductive_polymorphic_context mib)))
     else []
   in
-  let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
+  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
          Printer.pr_cumulative
@@ -183,7 +183,7 @@ let print_record env mind mib udecl =
   let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
-  let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
+  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0))
       (Array.to_list (Univ.Instance.to_array u)) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let keyword =
diff --git a/printing/printmod.mli b/printing/printmod.mli
index b0b0b0a35..48ba866cc 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -15,6 +15,6 @@ val printable_body : DirPath.t -> bool
 
 val pr_mutual_inductive_body : Environ.env ->
   MutInd.t -> Declarations.mutual_inductive_body ->
-  Universes.univ_name_list option -> Pp.t
+  UnivNames.univ_name_list option -> Pp.t
 val print_module : bool -> ModPath.t -> Pp.t
 val print_modtype : ModPath.t -> Pp.t