[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, 60 insertions, 51 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 018b51517..722dbc16b 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -2,6 +2,7 @@ open Printer
 open CErrors
 open Util
 open Term
+open Constr
 open Vars
 open Namegen
 open Names
@@ -80,7 +81,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let is_pte =
     let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in
     fun t ->
-      match kind_of_term t with
+      match Constr.kind t with
 	| Var id -> Id.Set.mem id set
 	| _ -> false
   in
@@ -100,13 +101,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let pre_princ = EConstr.Unsafe.to_constr pre_princ in
   let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
   let is_dom c =
-    match kind_of_term c with
+    match Constr.kind c with
       | Ind((u,_),_) -> MutInd.equal u rel_as_kn
       | Construct(((u,_),_),_) -> MutInd.equal u rel_as_kn
       | _ -> false
   in
   let get_fun_num c =
-    match kind_of_term c with
+    match Constr.kind c with
       | Ind((_,num),_) -> num
       | Construct(((_,num),_),_) -> num
       | _ -> assert false
@@ -119,7 +120,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   in
   let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
     let (new_princ_type,_) as res =
-      match kind_of_term pre_princ with
+      match Constr.kind pre_princ with
 	| Rel n ->
 	    begin
 	      try match Environ.lookup_rel n env with
@@ -149,12 +150,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	    in
 	    let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in
 	    applistc new_f new_args,
-	    list_union_eq eq_constr binders_to_remove_from_f binders_to_remove
+	    list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove
 	| LetIn(x,v,t,b) ->
 	    compute_new_princ_type_for_letin remove env x v t b
 	| _ -> pre_princ,[]
     in
-(*     let _ = match kind_of_term pre_princ with *)
+(*     let _ = match Constr.kind pre_princ with *)
 (* 	| Prod _ -> *)
 (* 	    observe(str "compute_new_princ_type for "++ *)
 (* 	      pr_lconstr_env env pre_princ ++ *)
@@ -170,13 +171,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	let new_x : Name.t = get_name (Termops.ids_of_context env) x in
 	let new_env = Environ.push_rel (LocalAssum (x,t)) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
-	 if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	 then (pop new_b), filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+	 if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
+	 then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
 	 else
 	   (
 	     bind_fun(new_x,new_t,new_b),
 	     list_union_eq
-	       eq_constr
+	       Constr.equal
 	       binders_to_remove_from_t
 	       (List.map pop binders_to_remove_from_b)
 	   )
@@ -189,7 +190,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	| Toberemoved_with_rel (n,c) ->
 (* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+	    new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b)
     end
   and compute_new_princ_type_for_letin remove env x v t b =
     begin
@@ -199,14 +200,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	let new_x : Name.t = get_name (Termops.ids_of_context env) x in
 	let new_env = Environ.push_rel (LocalDef (x,v,t)) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
-	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+	if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
+	then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
 	else
 	  (
 	    mkLetIn(new_x,new_v,new_t,new_b),
 	    list_union_eq
-	      eq_constr
-	      (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
+	      Constr.equal
+	      (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v)
 	      (List.map pop binders_to_remove_from_b)
 	  )
 
@@ -218,12 +219,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	| Toberemoved_with_rel (n,c) ->
 (* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+	    new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b)
     end
   and  compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc)  =
     let new_e,to_remove_from_e = compute_new_princ_type remove env e
     in
-    new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
+    new_e::c_acc,list_union_eq Constr.equal to_remove_from_e to_remove_acc
   in
 (*   observe (str "Computing new principe from " ++ pr_lconstr_env  env_with_params_and_predicates pre_princ); *)
   let pre_res,_ =
@@ -329,7 +330,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
       | Some (id) -> id,id
       | None ->
 	  let id_of_f = Label.to_id (Constant.label (fst f)) in
-	  id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
+	  id_of_f,Indrec.make_elimination_ident id_of_f (Sorts.family type_sort)
   in
   let names = ref [new_princ_name] in
   let hook =
@@ -389,7 +390,7 @@ exception Not_Rec
 
 let get_funs_constant mp dp =
   let get_funs_constant const e : (Names.Constant.t*int) array =
-    match kind_of_term ((strip_lam e)) with
+    match Constr.kind ((strip_lam e)) with
       | Fix((_,(na,_,_))) ->
 	  Array.mapi
 	    (fun i na ->
@@ -430,7 +431,7 @@ let get_funs_constant mp dp =
       let first_params = List.hd l_params  in
       List.iter
 	(fun params ->
-	   if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && eq_constr c1 c2) first_params params)
+	   if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && Constr.equal c1 c2) first_params params)
 	   then user_err Pp.(str "Not a mutal recursive block")
 	)
 	l_params
@@ -439,7 +440,7 @@ let get_funs_constant mp dp =
     let _check_bodies =
       try
 	let extract_info is_first body =
-	  match kind_of_term body with
+	  match Constr.kind body with
 	    | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
 	    | _ ->
 		if is_first && Int.equal (List.length l_bodies) 1
@@ -450,7 +451,7 @@ let get_funs_constant mp dp =
 	let check body  = (* Hope this is correct *)
 	  let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) =
             Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 &&
-            Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2
+            Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2
 	  in
 	  if not (eq_infos first_infos (extract_info false body))
 	  then  user_err Pp.(str "Not a mutal recursive block")
@@ -574,7 +575,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
 		let t =  (strip_prod_assum t) in
 		let applied_g = List.hd (List.rev (snd (decompose_app t))) in
 		let g = fst (decompose_app applied_g) in
-		if eq_constr f g
+		if Constr.equal f g
 		then raise (Found_type j);
 		observe (Printer.pr_lconstr f ++ str " <> " ++
 			   Printer.pr_lconstr g)
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 2eb1b7935..a3315f22c 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 
 val generate_functional_principle :
   Evd.evar_map ref -> 
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index e8e5bfccc..8ab6dbcdf 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -2,6 +2,7 @@ open Printer
 open Pp
 open Names
 open Term
+open Constr
 open Vars
 open Glob_term
 open Glob_ops
@@ -1015,7 +1016,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
 		    observe (str " computing new type for jmeq : done") ;
 		    let new_args =
-		      match kind_of_term eq'_as_constr with
+		      match Constr.kind eq'_as_constr with
 			| App(_,[|_;_;ty;_|]) ->
 			    let ty = Array.to_list (snd (destApp ty)) in
 			    let ty' = snd (Util.List.chop nparam ty) in
@@ -1297,7 +1298,7 @@ let rec rebuild_return_type rt =
 			    CAst.make @@ Constrexpr.CSort(GType []))
 
 let do_build_inductive
-      evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
+      evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
       returned_types
       (rtl:glob_constr list) =
   let _time1 = System.get_time () in
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 0cab5a6d3..ff0e98d00 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -11,7 +11,7 @@ val build_inductive :
   Id.t list -> (* The list of function name *) 
  *)
   Evd.evar_map ->
-  Term.pconstant list -> 
+  Constr.pconstant list -> 
   (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list list -> (* The list of function args *)
   Constrexpr.constr_expr list -> (* The list of function returned type *)
   Glob_term.glob_constr list -> (* the list of body *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 76fcd5ec8..e9102e9c8 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,8 +1,10 @@
 open Names
 open Pp
+open Constr
 open Libnames
 open Globnames
 open Refiner
+
 let mk_prefix pre id = Id.of_string (pre^(Id.to_string id))
 let mk_rel_id = mk_prefix "R_"
 let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
@@ -111,7 +113,7 @@ let const_of_id id =
       (str "cannot find " ++ Id.print id)
 
 let def_of_const t =
-   match (Term.kind_of_term t) with
+   match Constr.kind t with
     Term.Const sp ->
       (try (match Environ.constant_opt_value_in (Global.env()) sp with
              | Some c -> c
@@ -330,8 +332,6 @@ let discharge_Function (_,finfos) =
 	   is_general = finfos.is_general
 	 }
 
-open Term
-
 let pr_ocst c =
   Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ())
 
@@ -545,9 +545,9 @@ let prodn n env b =
 (* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *)
 let compose_prod l b = prodn (List.length l) l b
 
-type tcc_lemma_value = 
+type tcc_lemma_value =
   | Undefined
-  | Value of Term.constr
+  | Value of constr
   | Not_needed
 
 (* We only "purify" on exceptions *)
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index d41abee87..5cc7163aa 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -38,7 +38,7 @@ val chop_rlambda_n : int -> Glob_term.glob_constr ->
 val chop_rprod_n : int -> Glob_term.glob_constr ->
   (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr
 
-val def_of_const : Term.constr -> Term.constr
+val def_of_const : Constr.t -> Constr.t
 val eq : EConstr.constr Lazy.t
 val refl_equal : EConstr.constr Lazy.t
 val const_of_id: Id.t ->  Globnames.global_reference(* constantyes *)
@@ -118,10 +118,10 @@ val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
   (Names.Name.t * EConstr.t) list * EConstr.t
 val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
 val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
-                                                        
-type tcc_lemma_value = 
+
+type tcc_lemma_value =
   | Undefined
-  | Value of Term.constr
+  | Value of Constr.t
   | Not_needed
 
 val funind_purify : ('a -> 'b) -> ('a -> 'b)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 93317fce1..692a874d3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -12,6 +12,7 @@ open CErrors
 open Util
 open Names
 open Term
+open Constr
 open EConstr
 open Vars
 open Pp
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 77c26f8ce..b372241d2 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -18,6 +18,7 @@ open Vernacexpr
 open Pp
 open Names
 open Term
+open Constr
 open Vars
 open Declarations
 open Glob_term
@@ -36,19 +37,19 @@ let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
 
 (** Substitutions in constr *)
 let compare_constr_nosub t1 t2 =
-  if compare_constr (fun _ _ -> false) t1 t2
+  if Constr.compare_head (fun _ _ -> false) t1 t2
   then true
   else false
 
 let rec compare_constr' t1 t2 =
   if compare_constr_nosub t1 t2
   then true
-  else (compare_constr (compare_constr') t1 t2)
+  else (Constr.compare_head (compare_constr') t1 t2)
 
 let rec substitterm prof t by_t in_u =
   if (compare_constr' (lift prof t) in_u)
   then (lift prof by_t)
-  else map_constr_with_binders succ
+  else Constr.map_with_binders succ
     (fun i -> substitterm i t by_t) prof in_u
 
 let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl
@@ -954,16 +955,16 @@ let funify_branches relinfo nfuns branch =
       | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind
       | _ -> assert false in
   let is_dom c =
-    match kind_of_term c with
+    match Constr.kind c with
       | Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct
       | _ -> false in
   let _dom_i c =
     assert (is_dom c);
-    match kind_of_term c with
+    match Constr.kind c with
       | Ind((u,i)) | Construct((u,_),i) -> i
       | _ -> assert false in
   let _is_pred c shift =
-    match kind_of_term c with
+    match Constr.kind c with
       | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches)
       | _ -> false in
   (* FIXME: *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 76f859ed7..2fdc3bc37 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -10,6 +10,7 @@
 module CVars = Vars
 
 open Term
+open Constr
 open EConstr
 open Vars
 open Namegen
@@ -69,7 +70,7 @@ let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value =
 let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None)))
 
 let def_of_const t =
-   match (kind_of_term t) with
+   match (Constr.kind t) with
     Const sp ->
       (try (match constant_opt_value_in (Global.env ()) sp with
              | Some c -> c
@@ -143,7 +144,7 @@ let nat = function () -> (coq_init_constant "nat")
 let iter_ref () =  
   try find_reference ["Recdef"] "iter" 
   with Not_found -> user_err Pp.(str "module Recdef not loaded")
-let iter = function () -> (constr_of_global (delayed_force iter_ref))
+let iter_rd = function () -> (constr_of_global (delayed_force iter_ref))
 let eq = function () -> (coq_init_constant "eq")
 let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
 let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm")
@@ -175,8 +176,9 @@ let simpl_iter clause =
     clause
 
 (* Others ugly things ... *)
-let (value_f:Term.constr list -> global_reference -> Term.constr) =
+let (value_f: Constr.t list -> global_reference -> Constr.t) =
   let open Term in
+  let open Constr in
   fun al fterm ->
     let rev_x_id_l =
       (
@@ -207,7 +209,7 @@ let (value_f:Term.constr list -> global_reference -> Term.constr) =
     let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
     it_mkLambda_or_LetIn body context
 
-let (declare_f : Id.t -> logical_kind -> Term.constr list -> global_reference -> global_reference) =
+let (declare_f : Id.t -> logical_kind -> Constr.t list -> global_reference -> global_reference) =
   fun f_id kind input_type fterm_ref ->
     declare_fun f_id kind (value_f input_type fterm_ref);;
 
@@ -1039,11 +1041,12 @@ let prove_eq = travel equation_info
 *)
 let compute_terminate_type nb_args func =
   let open Term in
+  let open Constr in
   let open CVars in
   let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in
   let rev_args,b = decompose_prod_n nb_args a_arrow_b in
   let left =
-    mkApp(delayed_force iter,
+    mkApp(delayed_force iter_rd,
 	  Array.of_list
 	    (lift 5 a_arrow_b:: mkRel 3::
 	       constr_of_global func::mkRel 1::
@@ -1460,7 +1463,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
 
 let (com_eqn : int -> Id.t ->
        global_reference -> global_reference -> global_reference
-	 -> Term.constr -> unit) =
+	 -> Constr.t -> unit) =
   fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
     let open CVars in
     let opacity =
@@ -1514,6 +1517,7 @@ let (com_eqn : int -> Id.t ->
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
     generate_induction_principle using_lemmas : unit =
   let open Term in
+  let open Constr in
   let open CVars in
   let env = Global.env() in
   let evd = ref (Evd.from_env env) in
@@ -1536,7 +1540,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 (*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
 (*     Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)
 (*     Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *)
-    match kind_of_term eq' with
+    match Constr.kind eq' with
       | App(e,[|_;_;eq_fix|]) ->
 	  mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars  eq_fix))
       | _ -> failwith "Recursive Definition (res not eq)"
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 63bbdbe7e..50b84731b 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,3 +1,4 @@
+open Constr
 
 (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
 val tclUSER_if_not_mes : 
@@ -11,9 +12,9 @@ bool ->
            Constrintern.internalization_env ->
            Constrexpr.constr_expr ->
            Constrexpr.constr_expr ->
-           int -> Constrexpr.constr_expr -> (Term.pconstant ->
+           int -> Constrexpr.constr_expr -> (pconstant ->
             Indfun_common.tcc_lemma_value ref ->
-            Term.pconstant ->
-            Term.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit
+            pconstant ->
+            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit