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

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

10 files changed, 22 insertions, 21 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bd6aa0911..e1cf8f196 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -12,7 +12,7 @@ open CErrors
 open Util
 open Names
 open Nameops
-open Term
+open Constr
 open Termops
 open Libnames
 open Globnames
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b2df449c5..d980b1995 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Termops
 open EConstr
 open Environ
@@ -41,7 +40,7 @@ val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr
 val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
-val extern_sort : Evd.evar_map -> sorts -> glob_sort
+val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
   rel_context -> local_binder_expr list
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 75e99dd9b..46f96d20b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Evd
 open Environ
 open Libnames
diff --git a/interp/declare.ml b/interp/declare.ml
index 0ead94eff..0cc4d0fca 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -15,7 +15,7 @@ open Names
 open Libnames
 open Globnames
 open Nameops
-open Term
+open Constr
 open Declarations
 open Entries
 open Libobject
@@ -440,7 +440,7 @@ let assumption_message id =
 
 (** Global universe names, in a different summary *)
 
-type universe_context_decl = polymorphic * Univ.universe_context_set
+type universe_context_decl = polymorphic * Univ.ContextSet.t
 
 let cache_universe_context (p, ctx) =
   Global.push_context_set p ctx;
@@ -458,7 +458,7 @@ let declare_universe_context poly ctx =
   Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
 
 (* Discharged or not *)
-type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
+type universe_decl = polymorphic * (Id.t * Univ.Level.t) list
 
 let cache_universes (p, l) =
   let glob = Global.global_universe_names () in
diff --git a/interp/declare.mli b/interp/declare.mli
index 86d33cfb2..9b3194dec 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -8,7 +8,7 @@
 
 open Names
 open Libnames
-open Term
+open Constr
 open Entries
 open Decl_kinds
 
@@ -42,7 +42,7 @@ type internal_flag =
 (* Defaut definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
-  ?poly:polymorphic -> ?univs:Univ.universe_context ->
+  ?poly:polymorphic -> ?univs:Univ.UContext.t ->
   ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
 (** [declare_constant id cd] declares a global declaration
@@ -84,7 +84,7 @@ val exists_name : Id.t -> bool
 
 (** Global universe contexts, names and constraints *)
 
-val declare_universe_context : polymorphic -> Univ.universe_context_set -> unit
+val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
 
 val do_universe : polymorphic -> Id.t Loc.located list -> unit
 val do_constraint : polymorphic ->
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 0e4bbd299..5b4b5f67b 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -10,6 +10,7 @@ open Names
 open CErrors
 open Util
 open Term
+open Constr
 open Vars
 open Declarations
 open Cooking
diff --git a/interp/impargs.ml b/interp/impargs.ml
index daec1191e..72d22db4d 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -12,6 +12,7 @@ open Names
 open Globnames
 open Nameops
 open Term
+open Constr
 open Reduction
 open Declarations
 open Environ
@@ -167,7 +168,7 @@ let update pos rig (na,st) =
 
 (* modified is_rigid_reference with a truncated env *)
 let is_flexible_reference env bound depth f =
-  match kind_of_term f with
+  match kind f with
     | Rel n when n >= bound+depth -> (* inductive type *) false
     | Rel n when n >= depth -> (* previous argument *) true
     | Rel n -> (* since local definitions have been expanded *) false
@@ -191,7 +192,7 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
   let rec frec rig (env,depth as ed) c =
     let hd = if strict then whd_all env c else c in
     let c = if strongly_strict then hd else c in
-    match kind_of_term hd with
+    match kind hd with
     | Rel n when (n < bound+depth) && (n >= depth) ->
 	let i = bound + depth - n - 1 in
         acc.(i) <- update pos rig acc.(i)
@@ -214,13 +215,13 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
   let () = if not (Vars.noccur_between 1 bound m) then frec true (env,1) m in
   acc
 
-let rec is_rigid_head t = match kind_of_term t with
+let rec is_rigid_head t = match kind t with
   | Rel _ | Evar _ -> false
   | Ind _ | Const _ | Var _ | Sort _ -> true
   | Case (_,_,f,_) -> is_rigid_head f
   | Proj (p,c) -> true
   | App (f,args) ->
-      (match kind_of_term f with
+      (match kind f with
 	| Fix ((fi,i),_) -> is_rigid_head (args.(fi.(i)))
 	| _ -> is_rigid_head f)
   | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
@@ -240,7 +241,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let open Context.Rel.Declaration in
   let rec aux env avoid n names t =
     let t = whd_all env t in
-    match kind_of_term t with
+    match kind t with
       | Prod (na,a,b) ->
 	  let na',avoid' = find_displayed_name_in all avoid na (names,b) in
 	  add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
@@ -253,7 +254,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
 	    add_free_rels_until strict strongly_strict revpat n env t Conclusion v
 	  else v
   in
-  match kind_of_term (whd_all env t) with
+  match kind (whd_all env t) with
     | Prod (na,a,b) ->
 	let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in
 	let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 658d9e01a..40fa4cb26 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -7,8 +7,8 @@
 (************************************************************************)
 
 open Names
+open Constr
 open Globnames
-open Term
 open Environ
 
 (** {6 Implicit Arguments } *)
diff --git a/interp/notation.ml b/interp/notation.ml
index 076570c8a..f36294f73 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -11,7 +11,7 @@ open CErrors
 open Util
 open Pp
 open Names
-open Term
+open Constr
 open Libnames
 open Globnames
 open Constrexpr
@@ -653,7 +653,7 @@ let find_scope_class_opt = function
 (* Special scopes associated to arguments of a global reference *)
 
 let rec compute_arguments_classes t =
-  match kind_of_term (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with
+  match Constr.kind (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with
     | Prod (_,t,u) ->
 	let cl = try Some (compute_scope_class t) with Not_found -> None in
 	cl :: compute_arguments_classes u
diff --git a/interp/notation.mli b/interp/notation.mli
index e312a3767..2066d346f 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -165,8 +165,8 @@ val subst_scope_class :
 val declare_scope_class : scope_name -> scope_class -> unit
 val declare_ref_arguments_scope : global_reference -> unit
 
-val compute_arguments_scope : Term.types -> scope_name option list
-val compute_type_scope : Term.types -> scope_name option
+val compute_arguments_scope : Constr.types -> scope_name option list
+val compute_type_scope : Constr.types -> scope_name option
 
 (** Get the current scope bound to Sortclass, if it exists *)
 val current_type_scope_name : unit -> scope_name option