[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, 48 insertions, 45 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index ed612c0fc..e68087f14 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -10,6 +10,7 @@ open Equality
 open Names
 open Pp
 open Term
+open Constr
 open Termops
 open CErrors
 open Util
@@ -20,7 +21,7 @@ open Locus
 type rew_rule = { rew_lemma: constr;
 		  rew_type: types;
 		  rew_pat: constr;
-		  rew_ctx: Univ.universe_context_set;
+		  rew_ctx: Univ.ContextSet.t;
 		  rew_l2r: bool;
 		  rew_tac: Genarg.glob_generic_argument option }
 
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index edbb7c6b7..d2b5e070b 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -8,7 +8,7 @@
 
 (** This files implements the autorewrite tactic. *)
 
-open Term
+open Constr
 open Equality
 
 (** Rewriting rules before tactic interpretation *)
@@ -28,7 +28,7 @@ val autorewrite_in : ?conds:conditions -> Names.Id.t -> unit Proofview.tactic ->
 type rew_rule = { rew_lemma: constr;
 		  rew_type: types;
 		  rew_pat: constr;
-		  rew_ctx: Univ.universe_context_set;
+		  rew_ctx: Univ.ContextSet.t;
 		  rew_l2r: bool;
 		  rew_tac: Genarg.glob_generic_argument option }
 
@@ -58,5 +58,5 @@ type hypinfo = {
 
 val find_applied_relation :
   ?loc:Loc.t -> bool ->
-  Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo
+  Environ.env -> Evd.evar_map -> constr -> bool -> hypinfo
 
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 2d2a0c1b2..e427adb15 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -13,7 +13,8 @@
 
 (* This file builds schemes related to case analysis and recursion schemes *)
 
-open Term
+open Sorts
+open Constr
 open Indrec
 open Declarations
 open Typeops
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index e3fe7ddae..9c750e7ad 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -13,7 +13,7 @@ open Ind_tables
 val optimize_non_type_induction_scheme : 
   'a Ind_tables.scheme_kind ->
   Indrec.dep_flag ->
-  Term.sorts_family ->
+  Sorts.family ->
   'b ->
   Names.inductive ->
   (Constr.constr * Evd.evar_universe_context) * Safe_typing.private_constants
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index bfbac7787..d7667668e 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -48,6 +48,7 @@ open CErrors
 open Util
 open Names
 open Term
+open Constr
 open Vars
 open Declarations
 open Environ
@@ -106,8 +107,8 @@ let get_coq_eq ctx =
 
 let univ_of_eq env eq =
   let eq = EConstr.of_constr eq in
-  match kind_of_term (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with
-  | Prod (_,t,_) -> (match kind_of_term t with Sort (Type u) -> u | _ -> assert false)
+  match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with
+  | Prod (_,t,_) -> (match Constr.kind t with Sort (Type u) -> u | _ -> assert false)
   | _ -> assert false
 
 (**********************************************************************)
@@ -141,7 +142,7 @@ let get_sym_eq_data env (ind,u) =
   let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in
   let paramsctxt1,_ =
     List.chop (mib.mind_nparams-mip.mind_nrealargs) paramsctxt in
-  if not (List.equal Term.eq_constr params2 constrargs) then
+  if not (List.equal Constr.equal params2 constrargs) then
     error "Constructors arguments must repeat the parameters.";
   (* nrealargs_ctxt and nrealargs are the same here *)
   (specif,mip.mind_nrealargs,realsign,paramsctxt,paramsctxt1)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index 4acfa7a28..90ae67c6c 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -9,7 +9,7 @@
 (** This file builds schemes relative to equality inductive types *)
 
 open Names
-open Term
+open Constr
 open Environ
 open Ind_tables
 
@@ -22,14 +22,14 @@ val rew_l2r_forward_dep_scheme_kind : individual scheme_kind
 val rew_r2l_dep_scheme_kind : individual scheme_kind
 val rew_r2l_scheme_kind : individual scheme_kind
 
-val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> 
+val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family -> 
   constr Evd.in_evar_universe_context
-val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> 
+val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family -> 
   constr Evd.in_evar_universe_context * Safe_typing.private_constants
 val build_r2l_forward_rew_scheme :
-  bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context
+  bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context
 val build_l2r_forward_rew_scheme :
-  bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context
+  bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context
 
 (** Builds a symmetry scheme for a symmetrical equality type *)
 
@@ -43,5 +43,5 @@ val sym_involutive_scheme_kind : individual scheme_kind
 (** Builds a congruence scheme for an equality type *)
 
 val congr_scheme_kind : individual scheme_kind
-val build_congr : env -> constr * constr * Univ.universe_context_set -> inductive -> 
+val build_congr : env -> constr * constr * Univ.ContextSet.t -> inductive -> 
   constr Evd.in_evar_universe_context
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 3ccbab874..c7c53b393 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -128,14 +128,14 @@ type hints_path = global_reference hints_path_gen
 
 type hint_term =
   | IsGlobRef of global_reference
-  | IsConstr of constr * Univ.universe_context_set
+  | IsConstr of constr * Univ.ContextSet.t
 
 type 'a with_uid = {
   obj : 'a;
   uid : KerName.t;
 }
 
-type raw_hint = constr * types * Univ.universe_context_set
+type raw_hint = constr * types * Univ.ContextSet.t
 
 type hint = (raw_hint * clausenv) hint_ast with_uid
 
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 44e5370e9..22df29b80 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -42,7 +42,7 @@ type 'a hint_ast =
   | Extern     of Genarg.glob_generic_argument       (* Hint Extern *)
 
 type hint
-type raw_hint = constr * types * Univ.universe_context_set
+type raw_hint = constr * types * Univ.ContextSet.t
 
 type 'a hints_path_atom_gen =
   | PathHints of 'a list
@@ -146,7 +146,7 @@ type hint_info = (patvar list * constr_pattern) hint_info_gen
 
 type hint_term =
   | IsGlobRef of global_reference
-  | IsConstr of constr * Univ.universe_context_set
+  | IsConstr of constr * Univ.ContextSet.t
 
 type hints_entry =
   | HintsResolveEntry of
@@ -193,7 +193,7 @@ val prepare_hint : bool (* Check no remaining evars *) ->
 *)
 
 val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom ->
-  (constr * types * Univ.universe_context_set) -> hint_entry
+  (constr * types * Univ.ContextSet.t) -> hint_entry
 
 (** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))].
    [eapply] is true if this hint will be used only with EApply;
@@ -211,7 +211,7 @@ val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hint
 
 val make_apply_entry :
   env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
-  (constr * types * Univ.universe_context_set) -> hint_entry
+  (constr * types * Univ.ContextSet.t) -> hint_entry
 
 (** A constr which is Hint'ed will be:
    - (1) used as an Exact, if it does not start with a product
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 240b5a7e0..e7fa555c2 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -17,7 +17,7 @@ open Mod_subst
 open Libobject
 open Nameops
 open Declarations
-open Term
+open Constr
 open CErrors
 open Util
 open Declare
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 232a193ac..d73595a2f 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -6,8 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open Names
+open Constr
 open Declare
 
 (** This module provides support for registering inductive scheme builders,
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index fe733899f..cea6ccc30 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -10,7 +10,7 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
+open Constr
 open EConstr
 open Termops
 open Declarations
@@ -224,9 +224,8 @@ let compute_induction_names = compute_induction_names_gen true
 
 (* Compute the let-in signature of case analysis or standard induction scheme *)
 let compute_constructor_signatures isrec ((_,k as ity),u) =
-  let open Term in
   let rec analrec c recargs =
-    match kind_of_term c, recargs with
+    match Constr.kind c, recargs with
     | Prod (_,_,c), recarg::rest ->
         let rest = analrec c rest in
         begin match Declareops.dest_recarg recarg with
@@ -242,7 +241,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) =
   let (mib,mip) = Global.lookup_inductive ity in
   let n = mib.mind_nparams in
   let lc =
-    Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in
+    Array.map (fun c -> snd (Term.decompose_prod_n_assum n c)) mip.mind_nf_lc in
   let lrecargs = Declareops.dest_subterms mip.mind_recargs in
   Array.map2 analrec lc lrecargs
 
@@ -472,7 +471,7 @@ module New = struct
       let evi = Evd.find sigma evk in
       match Evd.evar_body evi with
       | Evd.Evar_empty -> Some (evk,evi)
-      | Evd.Evar_defined c -> match Term.kind_of_term c with
+      | Evd.Evar_defined c -> match Constr.kind c with
         | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
         | _ -> 
           (* We make the assumption that there is no way to refine an
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 3abd42d46..f5c209c74 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open EConstr
 open Tacmach
 open Proof_type
@@ -127,9 +127,9 @@ val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list arr
 val compute_induction_names :
   bool list array -> or_and_intro_pattern option -> intro_patterns array
 
-val elimination_sort_of_goal : goal sigma -> sorts_family
-val elimination_sort_of_hyp  : Id.t -> goal sigma -> sorts_family
-val elimination_sort_of_clause : Id.t option -> goal sigma -> sorts_family
+val elimination_sort_of_goal : goal sigma -> Sorts.family
+val elimination_sort_of_hyp  : Id.t -> goal sigma -> Sorts.family
+val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family
 
 val pf_with_evars :  (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
 val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
@@ -243,9 +243,9 @@ module New : sig
   val tryAllHypsAndConcl  : (Id.t option -> unit tactic) -> unit tactic
   val onClause   : (Id.t option -> unit tactic) -> clause -> unit tactic
 
-  val elimination_sort_of_goal : 'a Proofview.Goal.t -> sorts_family
-  val elimination_sort_of_hyp  : Id.t -> 'a Proofview.Goal.t -> sorts_family
-  val elimination_sort_of_clause : Id.t option -> 'a Proofview.Goal.t -> sorts_family
+  val elimination_sort_of_goal : 'a Proofview.Goal.t -> Sorts.family
+  val elimination_sort_of_hyp  : Id.t -> 'a Proofview.Goal.t -> Sorts.family
+  val elimination_sort_of_clause : Id.t option -> 'a Proofview.Goal.t -> Sorts.family
 
   val elimination_then :
     (branch_args -> unit Proofview.tactic) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 866daa904..ba244a794 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -14,6 +14,7 @@ open Util
 open Names
 open Nameops
 open Term
+open Constr
 open Termops
 open Environ
 open EConstr
@@ -1290,7 +1291,7 @@ let check_unresolved_evars_of_metas sigma clenv =
   (* Refiner.pose_all_metas_as_evars are resolved *)
   List.iter (fun (mv,b) -> match b with
   | Clval (_,(c,_),_) ->
-    (match kind_of_term c.rebus with
+    (match Constr.kind c.rebus with
     | Evar (evk,_) when Evd.is_undefined clenv.evd evk
                      && not (Evd.mem sigma evk) ->
       error_uninstantiated_metas (mkMeta mv) clenv
@@ -4958,7 +4959,7 @@ let interpretable_as_section_decl evd d1 d2 =
 let rec decompose len c t accu =
   let open Context.Rel.Declaration in
   if len = 0 then (c, t, accu)
-  else match kind_of_term c, kind_of_term t with 
+  else match Constr.kind c, Constr.kind t with 
   | Lambda (na, u, c), Prod (_, _, t) ->
     decompose (pred len) c t (LocalAssum (na, u) :: accu)
   | LetIn (na, b, u, c), LetIn (_, _, _, t) ->
@@ -4966,7 +4967,7 @@ let rec decompose len c t accu =
   | _ -> assert false
 
 let rec shrink ctx sign c t accu =
-  let open Term in
+  let open Constr in
   let open CVars in
   match ctx, sign with
   | [], [] -> (c, t, accu)
@@ -4976,8 +4977,8 @@ let rec shrink ctx sign c t accu =
         let t = subst1 mkProp t in
         shrink ctx sign c t accu
       else
-        let c = mkLambda_or_LetIn p c in
-        let t = mkProd_or_LetIn p t in
+        let c = Term.mkLambda_or_LetIn p c in
+        let t = Term.mkProd_or_LetIn p t in
         let accu = if RelDecl.is_local_assum p
                    then mkVar (NamedDecl.get_id decl) :: accu
                    else accu
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 98cf1b437..83fc655f1 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -8,7 +8,7 @@
 
 open Loc
 open Names
-open Term
+open Constr
 open EConstr
 open Environ
 open Proof_type
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 64ba38a51..6c8130d79 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -8,7 +8,7 @@
 
 (*i*)
 open Util
-open Term
+open Constr
 open Names
 open Globnames
 open Mod_subst
@@ -257,7 +257,7 @@ struct
   let pat_of_constr c : term_pattern =
     (** To each evar we associate a unique identifier. *)
     let metas = ref Evar.Map.empty in
-    let rec pat_of_constr c = match kind_of_term c with
+    let rec pat_of_constr c = match Constr.kind c with
     | Rel _          -> Term DRel
     | Sort _         -> Term DSort
     | Var i          -> Term (DRef (VarRef i))
@@ -290,7 +290,7 @@ struct
     | Proj (p,c) -> 
         Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c))
 
-    and ctx_of_constr ctx c = match kind_of_term c with
+    and ctx_of_constr ctx c = match Constr.kind c with
     | Prod (_,t,c)   -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c
     | LetIn(_,d,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t, Some (pat_of_constr d)),ctx))) c
     | _ -> ctx,pat_of_constr c
diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli
index 16122fa5e..db7da18ba 100644
--- a/tactics/term_dnet.mli
+++ b/tactics/term_dnet.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Constr
 open Mod_subst
 
 (** Dnets on constr terms.