Split off Universes functions dealing with names.

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

9 files changed, 213 insertions, 132 deletions

diff --git a/engine/engine.mllib b/engine/engine.mllib
index a5df5a9fa..207dbde1e 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,3 +1,4 @@
+UnivNames
 Universes
 Univops
 UState
diff --git a/engine/evd.mli b/engine/evd.mli
index 509db525d..7ce525744 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -550,7 +550,7 @@ val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
 
 
 val evar_universe_context_of_binders :
-  Universes.universe_binders -> UState.t
+  UnivNames.universe_binders -> UState.t
 [@@ocaml.deprecated "Alias of UState.of_binders"]
 
 val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t
@@ -559,7 +559,7 @@ val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> Id.t -> Univ.Level.t
 
-val universe_binders : evar_map -> Universes.universe_binders
+val universe_binders : evar_map -> UnivNames.universe_binders
 val add_constraints_context : UState.t ->
   Univ.Constraint.t -> UState.t
 [@@ocaml.deprecated "Alias of UState.add_constraints"]
diff --git a/engine/termops.ml b/engine/termops.ml
index df43be28e..9e975da58 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -47,7 +47,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
 
 let pr_puniverses p u = 
   if Univ.Instance.is_empty u then p 
-  else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+  else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
 
 let rec pr_constr c = match kind c with
   | Rel n -> str "#"++int n
diff --git a/engine/uState.ml b/engine/uState.ml
index df50bae86..ffb54d441 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -24,7 +24,7 @@ module UPairSet = Universes.UPairSet
 
 (* 2nd part used to check consistency on the fly. *)
 type t =
- { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t;
+ { uctx_names : UnivNames.universe_binders * uinfo Univ.LMap.t;
    uctx_local : Univ.ContextSet.t; (** The local context of variables *)
    uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *)
    uctx_univ_variables : Universes.universe_opt_subst;
@@ -298,7 +298,7 @@ let reference_of_level uctx =
     fun l ->
       try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname)
       with Not_found | Option.IsNone ->
-        Universes.reference_of_level l
+        UnivNames.reference_of_level l
 
 let pr_uctx_level uctx l =
   Libnames.pr_reference (reference_of_level uctx l)
diff --git a/engine/uState.mli b/engine/uState.mli
index 48c38fafc..b1fcefb0a 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -34,9 +34,9 @@ val union : t -> t -> t
 
 val of_context_set : Univ.ContextSet.t -> t
 
-val of_binders : Universes.universe_binders -> t
+val of_binders : UnivNames.universe_binders -> t
 
-val universe_binders : t -> Universes.universe_binders
+val universe_binders : t -> UnivNames.universe_binders
 
 (** {5 Projections} *)
 
diff --git a/engine/univNames.ml b/engine/univNames.ml
new file mode 100644
index 000000000..6e59a7c9e
--- /dev/null
+++ b/engine/univNames.ml
@@ -0,0 +1,105 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Univ
+open Globnames
+open Nametab
+
+
+let reference_of_level l = CAst.make @@
+  match Level.name l with
+  | Some (d, n as na)  ->
+     let qid =
+       try Nametab.shortest_qualid_of_universe na
+       with Not_found ->
+         let name = Id.of_string_soft (string_of_int n) in
+         Libnames.make_qualid d name
+     in Libnames.Qualid qid
+  | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l))
+
+let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l)
+
+(** Global universe information outside the kernel, to handle
+    polymorphic universe names in sections that have to be discharged. *)
+
+let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref)
+
+let add_global_universe u p =
+  match Level.name u with
+  | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map
+  | None -> ()
+
+let is_polymorphic l =
+  match Level.name l with
+  | Some n ->
+     (try Nametab.UnivIdMap.find n !universe_map
+      with Not_found -> false)
+  | None -> false
+
+(** Local universe names of polymorphic references *)
+
+type universe_binders = Univ.Level.t Names.Id.Map.t
+
+let empty_binders = Id.Map.empty
+
+let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
+
+let universe_binders_of_global ref : universe_binders =
+  try
+    let l = Refmap.find ref !universe_binders_table in l
+  with Not_found -> Names.Id.Map.empty
+
+let cache_ubinder (_,(ref,l)) =
+  universe_binders_table := Refmap.add ref l !universe_binders_table
+
+let subst_ubinder (subst,(ref,l as orig)) =
+  let ref' = fst (Globnames.subst_global subst ref) in
+  if ref == ref' then orig else ref', l
+
+let discharge_ubinder (_,(ref,l)) =
+  Some (Lib.discharge_global ref, l)
+
+let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
+  let open Libobject in
+  declare_object { (default_object "universe binder") with
+    cache_function = cache_ubinder;
+    load_function = (fun _ x -> cache_ubinder x);
+    classify_function = (fun x -> Substitute x);
+    subst_function = subst_ubinder;
+    discharge_function = discharge_ubinder;
+    rebuild_function = (fun x -> x); }
+
+let register_universe_binders ref ubinders =
+  (* Add the polymorphic (section) universes *)
+  let ubinders = UnivIdMap.fold (fun lvl poly ubinders ->
+    let qid = Nametab.shortest_qualid_of_universe lvl in
+    let level = Level.make (fst lvl) (snd lvl) in
+    if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders
+    else ubinders)
+    !universe_map ubinders
+  in
+  if not (Id.Map.is_empty ubinders)
+  then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
+
+type univ_name_list = Misctypes.lname list
+
+let universe_binders_with_opt_names ref levels = function
+  | None -> universe_binders_of_global ref
+  | Some udecl ->
+    if Int.equal(List.length levels) (List.length udecl)
+    then
+      List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with
+          | Anonymous -> acc
+          | Name na -> Names.Id.Map.add na lvl acc)
+        empty_binders udecl levels
+    else
+      CErrors.user_err ~hdr:"universe_binders_with_opt_names"
+        Pp.(str "Universe instance should have length " ++ int (List.length levels))
diff --git a/engine/univNames.mli b/engine/univNames.mli
new file mode 100644
index 000000000..e3bc3193d
--- /dev/null
+++ b/engine/univNames.mli
@@ -0,0 +1,41 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Univ
+
+val pr_with_global_universes : Level.t -> Pp.t
+val reference_of_level : Level.t -> Libnames.reference
+
+(** Global universe information outside the kernel, to handle
+    polymorphic universes in sections that have to be discharged. *)
+val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
+
+(** Is [lvl]  a global polymorphic universe? (ie section polymorphic universe) *)
+val is_polymorphic : Level.t -> bool
+
+(** Local universe name <-> level mapping *)
+
+type universe_binders = Univ.Level.t Names.Id.Map.t
+
+val empty_binders : universe_binders
+
+val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
+val universe_binders_of_global : Names.GlobRef.t -> universe_binders
+
+type univ_name_list = Misctypes.lname list
+
+(** [universe_binders_with_opt_names ref u l]
+
+    If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous).
+    May error if the lengths mismatch.
+
+    Otherwise return [universe_binders_of_global ref]. *)
+val universe_binders_with_opt_names : Names.GlobRef.t ->
+  Univ.Level.t list -> univ_name_list option -> universe_binders
diff --git a/engine/universes.ml b/engine/universes.ml
index 96d49361f..1dccde025 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -15,102 +15,6 @@ open Names
 open Constr
 open Environ
 open Univ
-open Globnames
-open Nametab
-
-module UPairs = OrderedType.UnorderedPair(Univ.Level)
-module UPairSet = Set.Make (UPairs)
-
-let reference_of_level l = CAst.make @@
-  match Level.name l with
-  | Some (d, n as na)  ->
-     let qid =
-       try Nametab.shortest_qualid_of_universe na
-       with Not_found ->
-         let name = Id.of_string_soft (string_of_int n) in
-         Libnames.make_qualid d name
-     in Libnames.Qualid qid
-  | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l))
-
-let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l)
-
-(** Global universe information outside the kernel, to handle
-    polymorphic universe names in sections that have to be discharged. *)
-
-let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref)
-
-let add_global_universe u p =
-  match Level.name u with
-  | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map
-  | None -> ()
-
-let is_polymorphic l =
-  match Level.name l with
-  | Some n ->
-     (try Nametab.UnivIdMap.find n !universe_map
-      with Not_found -> false)
-  | None -> false
-
-(** Local universe names of polymorphic references *)
-
-type universe_binders = Univ.Level.t Names.Id.Map.t
-
-let empty_binders = Id.Map.empty
-
-let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
-
-let universe_binders_of_global ref : universe_binders =
-  try
-    let l = Refmap.find ref !universe_binders_table in l
-  with Not_found -> Names.Id.Map.empty
-
-let cache_ubinder (_,(ref,l)) =
-  universe_binders_table := Refmap.add ref l !universe_binders_table
-
-let subst_ubinder (subst,(ref,l as orig)) =
-  let ref' = fst (Globnames.subst_global subst ref) in
-  if ref == ref' then orig else ref', l
-
-let discharge_ubinder (_,(ref,l)) =
-  Some (Lib.discharge_global ref, l)
-
-let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
-  let open Libobject in
-  declare_object { (default_object "universe binder") with
-    cache_function = cache_ubinder;
-    load_function = (fun _ x -> cache_ubinder x);
-    classify_function = (fun x -> Substitute x);
-    subst_function = subst_ubinder;
-    discharge_function = discharge_ubinder;
-    rebuild_function = (fun x -> x); }
-
-let register_universe_binders ref ubinders =
-  let open Names in
-  (* Add the polymorphic (section) universes *)
-  let ubinders = UnivIdMap.fold (fun lvl poly ubinders ->
-    let qid = Nametab.shortest_qualid_of_universe lvl in
-    let level = Level.make (fst lvl) (snd lvl) in
-    if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders
-    else ubinders)
-    !universe_map ubinders
-  in
-  if not (Id.Map.is_empty ubinders)
-  then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
-
-type univ_name_list = Misctypes.lname list
-
-let universe_binders_with_opt_names ref levels = function
-  | None -> universe_binders_of_global ref
-  | Some udecl ->
-    if Int.equal(List.length levels) (List.length udecl)
-    then
-      List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with
-          | Anonymous -> acc
-          | Name na -> Names.Id.Map.add na lvl acc)
-        empty_binders udecl levels
-    else
-      CErrors.user_err ~hdr:"universe_binders_with_opt_names"
-        Pp.(str "Universe instance should have length " ++ int (List.length levels))
 
 (* To disallow minimization to Set *)
 
@@ -917,6 +821,9 @@ let minimize_univ_variables ctx us algs left right cstrs =
       else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs)
       us (ctx, us, algs, lbounds, cstrs)
 
+module UPairs = OrderedType.UnorderedPair(Univ.Level)
+module UPairSet = Set.Make (UPairs)
+
 let normalize_context_set g ctx us algs weak =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   (** Keep the Prop/Set <= i constraints separate for minimization *)
@@ -1111,3 +1018,21 @@ let solve_constraints_system levels level_bounds level_min =
     done;
   done;
   v
+
+(** Deprecated *)
+type universe_binders = UnivNames.universe_binders
+type univ_name_list = UnivNames.univ_name_list
+
+let pr_with_global_universes = UnivNames.pr_with_global_universes
+let reference_of_level = UnivNames.reference_of_level
+
+let add_global_universe = UnivNames.add_global_universe
+
+let is_polymorphic = UnivNames.is_polymorphic
+
+let empty_binders = UnivNames.empty_binders
+
+let register_universe_binders = UnivNames.register_universe_binders
+let universe_binders_of_global = UnivNames.universe_binders_of_global
+
+let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names
diff --git a/engine/universes.mli b/engine/universes.mli
index 46d65f257..aaf295c1d 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -19,35 +19,6 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t)
 
 (** Universes *)
 
-val pr_with_global_universes : Level.t -> Pp.t
-val reference_of_level : Level.t -> Libnames.reference
-
-(** Global universe information outside the kernel, to handle
-    polymorphic universes in sections that have to be discharged. *)
-val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
-
-val is_polymorphic : Level.t -> bool
-
-(** Local universe name <-> level mapping *)
-
-type universe_binders = Univ.Level.t Names.Id.Map.t
-
-val empty_binders : universe_binders
-
-val register_universe_binders : GlobRef.t -> universe_binders -> unit
-val universe_binders_of_global : GlobRef.t -> universe_binders
-
-type univ_name_list = Misctypes.lname list
-
-(** [universe_binders_with_opt_names ref u l]
-
-    If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous).
-    May error if the lengths mismatch.
-
-    Otherwise return [universe_binders_of_global ref]. *)
-val universe_binders_with_opt_names : Names.GlobRef.t ->
-  Univ.Level.t list -> univ_name_list option -> universe_binders
-
 (** The global universe counter *)
 type universe_id = DirPath.t * int
 
@@ -226,3 +197,41 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.t
 
 val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array ->
   Universe.t array
+
+(** *********************************** Deprecated *)
+[@@@ocaml.warning "-3"]
+val set_minimization : bool ref
+[@@ocaml.deprecated "Becoming internal."]
+val is_set_minimization : unit -> bool
+[@@ocaml.deprecated "Becoming internal."]
+
+(** ****** Deprecated: moved to [UnivNames] *)
+
+val pr_with_global_universes : Level.t -> Pp.t
+[@@ocaml.deprecated "Use [UnivNames.pr_with_global_universes]"]
+val reference_of_level : Level.t -> Libnames.reference
+[@@ocaml.deprecated "Use [UnivNames.reference_of_level]"]
+
+val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
+[@@ocaml.deprecated "Use [UnivNames.add_global_universe]"]
+
+val is_polymorphic : Level.t -> bool
+[@@ocaml.deprecated "Use [UnivNames.is_polymorphic]"]
+
+type universe_binders = UnivNames.universe_binders
+[@@ocaml.deprecated "Use [UnivNames.universe_binders]"]
+
+val empty_binders : universe_binders
+[@@ocaml.deprecated "Use [UnivNames.empty_binders]"]
+
+val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
+[@@ocaml.deprecated "Use [UnivNames.register_universe_binders]"]
+val universe_binders_of_global : Globnames.global_reference -> universe_binders
+[@@ocaml.deprecated "Use [UnivNames.universe_binders_of_global]"]
+
+type univ_name_list = UnivNames.univ_name_list
+[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"]
+
+val universe_binders_with_opt_names : Globnames.global_reference ->
+  Univ.Level.t list -> univ_name_list option -> universe_binders
+[@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"]