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

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

5 files changed, 23 insertions, 22 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 3c46d5c43..bc84df76b 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Miniml
-open Term
+open Constr
 open Declarations
 open Names
 open ModPath
@@ -138,7 +138,7 @@ let check_arity env cb =
 let check_fix env cb i =
   match cb.const_body with
     | Def lbody ->
-	(match kind_of_term (Mod_subst.force_constr lbody) with
+	(match Constr.kind (Mod_subst.force_constr lbody) with
 	  | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
 	  | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd)
 	  | _ -> raise Impossible)
@@ -146,8 +146,8 @@ let check_fix env cb i =
 
 let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) =
   Array.equal Name.equal na1 na2 &&
-  Array.equal eq_constr ca1 ca2 &&
-  Array.equal eq_constr ta1 ta2
+  Array.equal Constr.equal ca1 ca2 &&
+  Array.equal Constr.equal ta1 ta2
 
 let factor_fix env l cb msb =
   let _,recd as check = check_fix env cb 0 in
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 7bbb825b1..dd8617738 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -34,4 +34,4 @@ val print_one_decl :
 (* Used by Extraction Compute *)
 
 val structure_for_compute :
-  Term.constr -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type
+  Constr.t -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a227478d0..47e812319 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -10,6 +10,7 @@
 open Util
 open Names
 open Term
+open Constr
 open Vars
 open Declarations
 open Declareops
@@ -81,7 +82,7 @@ let whd_betaiotazeta t =
 
 let rec flag_of_type env t : flag =
   let t = whd_all env t in
-  match kind_of_term t with
+  match Constr.kind t with
     | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c
     | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
     | Sort _ -> (Info,TypeScheme)
@@ -111,14 +112,14 @@ let push_rel_assum (n, t) env =
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
 let rec type_sign env c =
-  match kind_of_term (whd_all env c) with
+  match Constr.kind (whd_all env c) with
     | Prod (n,t,d) ->
 	(if is_info_scheme env t then Keep else Kill Kprop)
 	:: (type_sign (push_rel_assum (n,t) env) d)
     | _ -> []
 
 let rec type_scheme_nb_args env c =
-  match kind_of_term (whd_all env c) with
+  match Constr.kind (whd_all env c) with
     | Prod (n,t,d) ->
 	let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in
 	if is_info_scheme env t then n+1 else n
@@ -145,7 +146,7 @@ let make_typvar n vl =
   next_ident_away id' vl
 
 let rec type_sign_vl env c =
-  match kind_of_term (whd_all env c) with
+  match Constr.kind (whd_all env c) with
     | Prod (n,t,d) ->
 	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
 	if not (is_info_scheme env t) then Kill Kprop::s, vl
@@ -153,7 +154,7 @@ let rec type_sign_vl env c =
     | _ -> [],[]
 
 let rec nb_default_params env c =
-  match kind_of_term (whd_all env c) with
+  match Constr.kind (whd_all env c) with
     | Prod (n,t,d) ->
 	let n = nb_default_params (push_rel_assum (n,t) env) d in
 	if is_default env t then n+1 else n
@@ -207,7 +208,7 @@ let parse_ind_args si args relmax =
     | [] -> Int.Map.empty
     | Kill _ :: s -> parse (i+1) j s
     | Keep :: s ->
-      (match kind_of_term args.(i-1) with
+      (match Constr.kind args.(i-1) with
 	 | Rel k -> Int.Map.add (relmax+1-k) j (parse (i+1) (j+1) s)
 	 | _ -> parse (i+1) (j+1) s)
   in parse 1 1 si
@@ -224,7 +225,7 @@ let parse_ind_args si args relmax =
 
 
 let rec extract_type env db j c args =
-  match kind_of_term (whd_betaiotazeta c) with
+  match Constr.kind (whd_betaiotazeta c) with
     | App (d, args') ->
 	(* We just accumulate the arguments. *)
 	extract_type env db j d (Array.to_list args' @ args)
@@ -299,7 +300,7 @@ let rec extract_type env db j c args =
     | Proj (p,t) ->
        (* Let's try to reduce, if it hasn't already been done. *)
        if Projection.unfolded p then Tunknown
-       else extract_type env db j (Term.mkProj (Projection.unfold p, t)) args
+       else extract_type env db j (mkProj (Projection.unfold p, t)) args
     | Case _ | Fix _ | CoFix _ -> Tunknown
     | _ -> assert false
 
@@ -331,7 +332,7 @@ and extract_type_scheme env db c p =
   if Int.equal p 0 then extract_type env db 0 c []
   else
     let c = whd_betaiotazeta c in
-    match kind_of_term c with
+    match Constr.kind c with
       | Lambda (n,t,d) ->
           extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
       | _ ->
@@ -415,8 +416,8 @@ and extract_really_ind env kn mib =
 	  let t = snd (decompose_prod_n npar types.(j)) in
 	  let prods,head = dest_prod epar t in
 	  let nprods = List.length prods in
-          let args = match kind_of_term head with
-            | App (f,args) -> args (* [kind_of_term f = Ind ip] *)
+          let args = match Constr.kind head with
+            | App (f,args) -> args (* [Constr.kind f = Ind ip] *)
             | _ -> [||]
           in
 	  let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in
@@ -444,7 +445,7 @@ and extract_really_ind env kn mib =
 	if Option.is_empty mib.mind_record then raise (I Standard);
 	(* Now we're sure it's a record. *)
 	(* First, we find its field names. *)
-	let rec names_prod t = match kind_of_term t with
+	let rec names_prod t = match Constr.kind t with
 	  | Prod(n,_,t) -> n::(names_prod t)
 	  | LetIn(_,_,_,t) -> names_prod t
 	  | Cast(t,_,_) -> names_prod t
@@ -503,7 +504,7 @@ and extract_really_ind env kn mib =
 *)
 
 and extract_type_cons env db dbmap c i =
-  match kind_of_term (whd_all env c) with
+  match Constr.kind (whd_all env c) with
     | Prod (n,t,d) ->
 	let env' = push_rel_assum (n,t) env in
 	let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in
@@ -564,7 +565,7 @@ let record_constant_type env kn opt_typ =
 (* [mlt] is the ML type we want our extraction of [(c args)] to have. *)
 
 let rec extract_term env mle mlt c args =
-  match kind_of_term c with
+  match Constr.kind c with
     | App (f,a) ->
 	extract_term env mle mlt f (Array.to_list a @ args)
     | Lambda (n, t, d) ->
@@ -874,7 +875,7 @@ let decomp_lams_eta_n n m env c t =
 (* Let's try to identify some situation where extracted code
    will allow generalisation of type variables *)
 
-let rec gentypvar_ok c = match kind_of_term c with
+let rec gentypvar_ok c = match Constr.kind c with
   | Lambda _ | Const _ -> true
   | App (c,v) ->
       (* if all arguments are variables, these variables will
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index e1d43f340..b15b88ed2 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -9,7 +9,7 @@
 (*s Extraction from Coq terms to Miniml. *)
 
 open Names
-open Term
+open Constr
 open Declarations
 open Environ
 open Miniml
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index cc93f294b..e52e419fd 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -180,7 +180,7 @@ val implicits_of_global : global_reference -> Int.Set.t
 (*s Table for user-given custom ML extractions. *)
 
 (* UGLY HACK: registration of a function defined in [extraction.ml] *)
-val type_scheme_nb_args_hook : (Environ.env -> Term.constr -> int) Hook.t
+val type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t
 
 val is_custom : global_reference -> bool
 val is_inline_custom : global_reference -> bool