[api] Move structures deprecated in the API to the core.

We do up to `Term` which is the main bulk of the changes.

16 files changed, 42 insertions, 41 deletions

diff --git a/library/declaremods.mli b/library/declaremods.mli
index 90e86cd02..42e5f4b13 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -72,7 +72,7 @@ type library_objects
 val register_library :
   library_name ->
   Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest ->
-  Univ.universe_context_set -> unit
+  Univ.ContextSet.t -> unit
 
 val get_library_native_symbols : library_name -> Nativecode.symbols
 
diff --git a/library/decls.ml b/library/decls.ml
index 973fe144d..a4259f6ca 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -19,7 +19,7 @@ module NamedDecl = Context.Named.Declaration
 (** Datas associated to section variables and local definitions *)
 
 type variable_data =
-  DirPath.t * bool (* opacity *) * Univ.universe_context_set * polymorphic * logical_kind
+  DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
 
 let vartab =
   Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE"
diff --git a/library/decls.mli b/library/decls.mli
index 524377257..1b7f137a4 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -17,14 +17,14 @@ open Decl_kinds
 (** Registration and access to the table of variable *)
 
 type variable_data =
-  DirPath.t * bool (** opacity *) * Univ.universe_context_set * polymorphic * logical_kind
+  DirPath.t * bool (** opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
 
 val add_variable_data : variable -> variable_data -> unit
 val variable_path : variable -> DirPath.t
 val variable_secpath : variable -> qualid
 val variable_kind : variable -> logical_kind
 val variable_opacity : variable -> bool
-val variable_context : variable -> Univ.universe_context_set
+val variable_context : variable -> Univ.ContextSet.t
 val variable_polymorphic : variable -> polymorphic
 val variable_exists : variable -> bool
 
diff --git a/library/global.ml b/library/global.ml
index 28b9e66f8..43097dc5d 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -233,7 +233,7 @@ let universes_of_global gr =
 
 (** Global universe names *)
 type universe_names = 
-  (polymorphic * Univ.universe_level) Id.Map.t * Id.t Univ.LMap.t
+  (polymorphic * Univ.Level.t) Id.Map.t * Id.t Univ.LMap.t
 
 let global_universes =
   Summary.ref ~name:"Global universe names"
diff --git a/library/global.mli b/library/global.mli
index 1aff0a376..51fe53181 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -32,7 +32,7 @@ val set_typing_flags : Declarations.typing_flags -> unit
 (** Variables, Local definitions, constants, inductive types *)
 
 val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
-val push_named_def   : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set
+val push_named_def   : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.ContextSet.t
 
 val export_private_constants : in_section:bool ->
   Safe_typing.private_constants Entries.constant_entry ->
@@ -46,8 +46,8 @@ val add_mind :
 (** Extra universe constraints *)
 val add_constraints : Univ.constraints -> unit
 
-val push_context : bool -> Univ.universe_context -> unit
-val push_context_set : bool -> Univ.universe_context_set -> unit
+val push_context : bool -> Univ.UContext.t -> unit
+val push_context_set : bool -> Univ.ContextSet.t -> unit
 
 (** Non-interactive modules and module types *)
 
@@ -93,18 +93,18 @@ val mind_of_delta_kn : KerName.t -> MutInd.t
 
 val opaque_tables : unit -> Opaqueproof.opaquetab
 
-val body_of_constant : Constant.t -> (Term.constr * Univ.AUContext.t) option
+val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option
 (** Returns the body of the constant if it has any, and the polymorphic context
     it lives in. For monomorphic constant, the latter is empty, and for
     polymorphic constants, the term contains De Bruijn universe variables that
     need to be instantiated. *)
 
-val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option
+val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
 (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
 
 (** Global universe name <-> level mapping *)
 type universe_names = 
-  (Decl_kinds.polymorphic * Univ.universe_level) Id.Map.t * Id.t Univ.LMap.t
+  (Decl_kinds.polymorphic * Univ.Level.t) Id.Map.t * Id.t Univ.LMap.t
 
 val global_universe_names : unit -> universe_names
 val set_global_universe_names : universe_names -> unit
@@ -115,7 +115,7 @@ val start_library : DirPath.t -> ModPath.t
 val export : ?except:Future.UUIDSet.t -> DirPath.t ->
   ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library
 val import :
-  Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest ->
+  Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest ->
   ModPath.t
 
 (** {6 Misc } *)
@@ -147,12 +147,12 @@ val type_of_global_in_context : Environ.env ->
     constants, it does not matter. *)
 
 (** Returns the universe context of the global reference (whatever its polymorphic status is). *)
-val universes_of_global : Globnames.global_reference -> Univ.abstract_universe_context
+val universes_of_global : Globnames.global_reference -> Univ.AUContext.t
 
 (** {6 Retroknowledge } *)
 
 val register :
-  Retroknowledge.field -> Term.constr -> Term.constr -> unit
+  Retroknowledge.field -> Constr.constr -> Constr.constr -> unit
 
 val register_inline : Constant.t -> unit
 
diff --git a/library/globnames.ml b/library/globnames.ml
index 9f652896c..9d7ab2db8 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -8,7 +8,7 @@
 
 open CErrors
 open Names
-open Term
+open Constr
 open Mod_subst
 open Libnames
 
@@ -72,7 +72,7 @@ let canonical_gr = function
   | ConstructRef ((kn,i),j )-> ConstructRef((MutInd.make1(MutInd.canonical kn),i),j)
   | VarRef id -> VarRef id
 
-let global_of_constr c = match kind_of_term c with
+let global_of_constr c = match kind c with
   | Const (sp,u) -> ConstRef sp
   | Ind (ind_sp,u) -> IndRef ind_sp
   | Construct (cstr_cp,u) -> ConstructRef cstr_cp
@@ -80,7 +80,7 @@ let global_of_constr c = match kind_of_term c with
   |  _ -> raise Not_found
 
 let is_global c t =
-  match c, kind_of_term t with
+  match c, kind t with
   | ConstRef c, Const (c', _) -> Constant.equal c c'
   | IndRef i, Ind (i', _) -> eq_ind i i'
   | ConstructRef i, Construct (i', _) -> eq_constructor i i'
diff --git a/library/globnames.mli b/library/globnames.mli
index 361631bd3..5c484b391 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -8,7 +8,7 @@
 
 open Util
 open Names
-open Term
+open Constr
 open Mod_subst
 
 (** {6 Global reference is a kernel side type for all references together } *)
diff --git a/library/heads.ml b/library/heads.ml
index d2cfc0990..8b8e407f7 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -9,6 +9,7 @@
 open Util
 open Names
 open Term
+open Constr
 open Vars
 open Mod_subst
 open Environ
@@ -57,7 +58,7 @@ let variable_head id  = Evalrefmap.find (EvalVarRef id) !head_map
 let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map
 
 let kind_of_head env t =
-  let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta env t) with
+  let rec aux k l t b = match kind (Reduction.whd_betaiotazeta env t) with
   | Rel n when n > k -> NotImmediatelyComputableHead
   | Rel n -> FlexibleHead (k,k+1-n,List.length l,b)
   | Var id ->
diff --git a/library/heads.mli b/library/heads.mli
index 1ce66c841..8ad5c0f14 100644
--- a/library/heads.mli
+++ b/library/heads.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 
 (** This module is about the computation of an approximation of the
diff --git a/library/lib.ml b/library/lib.ml
index a6fa27be8..df9563e45 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -417,8 +417,8 @@ type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
 type secentry =
   | Variable of (Names.Id.t * Decl_kinds.binding_kind *
-		   Decl_kinds.polymorphic * Univ.universe_context_set)
-  | Context of Univ.universe_context_set
+		   Decl_kinds.polymorphic * Univ.ContextSet.t)
+  | Context of Univ.ContextSet.t
 
 let sectab =
   Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list)
diff --git a/library/lib.mli b/library/lib.mli
index f941fd6d4..721e2896f 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -162,11 +162,11 @@ val section_segment_of_constant : Names.Constant.t -> abstr_info
 val section_segment_of_mutual_inductive: Names.MutInd.t -> abstr_info
 val variable_section_segment_of_reference : Globnames.global_reference -> variable_context
 
-val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array
+val section_instance : Globnames.global_reference -> Univ.Instance.t * Names.Id.t array
 val is_in_section : Globnames.global_reference -> bool
 
-val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit
-val add_section_context : Univ.universe_context_set -> unit
+val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
+val add_section_context : Univ.ContextSet.t -> unit
 val add_section_constant : Decl_kinds.polymorphic ->
   Names.Constant.t -> Context.Named.t -> unit
 val add_section_kn : Decl_kinds.polymorphic ->
diff --git a/library/library.ml b/library/library.ml
index e2832ecdc..840fe563a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -97,7 +97,7 @@ type library_t = {
   library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
   library_imports : compilation_unit_name array;
   library_digests : Safe_typing.vodigest;
-  library_extra_univs : Univ.universe_context_set;
+  library_extra_univs : Univ.ContextSet.t;
 }
 
 type library_summary = {
@@ -360,9 +360,9 @@ type 'a table_status =
   | Fetched of 'a Future.computation array
 
 let opaque_tables =
-  ref (LibraryMap.empty : (Term.constr table_status) LibraryMap.t)
+  ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
 let univ_tables =
-  ref (LibraryMap.empty : (Univ.universe_context_set table_status) LibraryMap.t)
+  ref (LibraryMap.empty : (Univ.ContextSet.t table_status) LibraryMap.t)
 
 let add_opaque_table dp st =
   opaque_tables := LibraryMap.add dp st !opaque_tables
@@ -408,9 +408,9 @@ let () =
 type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
-  Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool
+  Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Term.constr Future.computation array
+type seg_proofs = Constr.constr Future.computation array
 
 let mk_library sd md digests univs =
   {
diff --git a/library/library.mli b/library/library.mli
index 6c624ce52..63e7b95bb 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -29,9 +29,9 @@ val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> u
 type seg_sum
 type seg_lib
 type seg_univ = (* cst, all_cst, finished? *)
-  Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool
+  Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Term.constr Future.computation array
+type seg_proofs = Constr.constr Future.computation array
 
 (** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
diff --git a/library/nameops.mli b/library/nameops.mli
index 58cd6ed4e..26f300b61 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -131,5 +131,5 @@ val coq_string : string (** "Coq" *)
 val default_root_prefix : DirPath.t
 
 (** Metavariables *)
-val pr_meta : Term.metavariable -> Pp.t
-val string_of_meta : Term.metavariable -> string
+val pr_meta : Constr.metavariable -> Pp.t
+val string_of_meta : Constr.metavariable -> string
diff --git a/library/univops.ml b/library/univops.ml
index 3bafb824d..9dc138eb8 100644
--- a/library/univops.ml
+++ b/library/univops.ml
@@ -6,18 +6,18 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Constr
 open Univ
 
 let universes_of_constr c =
   let rec aux s c = 
-    match kind_of_term c with
+    match kind c with
     | Const (_, u) | Ind (_, u) | Construct (_, u) ->
       LSet.fold LSet.add (Instance.levels u) s
     | Sort u when not (Sorts.is_small u) -> 
-      let u = univ_of_sort u in
+      let u = Term.univ_of_sort u in
       LSet.fold LSet.add (Universe.levels u) s
-    | _ -> fold_constr aux s c
+    | _ -> Constr.fold aux s c
   in aux LSet.empty c
 
 let restrict_universe_context (univs,csts) s =
diff --git a/library/univops.mli b/library/univops.mli
index 09147cb41..9af568bcb 100644
--- a/library/univops.mli
+++ b/library/univops.mli
@@ -6,10 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Constr
 open Univ
 
 (** Shrink a universe context to a restricted set of variables *)
 
-val universes_of_constr : constr -> universe_set
-val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set
+val universes_of_constr : constr -> LSet.t
+val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t