Merge PR #6098: [api] Move structures deprecated in the API to the core.

12 files changed, 23 insertions, 22 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 9c69995f4..9a2026dd3 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -11,7 +11,7 @@
     evar-based clauses. *)
 
 open Names
-open Term
+open Constr
 open Environ
 open Evd
 open EConstr
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 61f3e4a02..19f816a01 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -99,7 +99,7 @@ module V82 = struct
   let same_goal evars1 gl1 evars2 gl2 =
     let evi1 = Evd.find evars1 gl1 in
     let evi2 = Evd.find evars2 gl2 in
-    Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl &&
+    Constr.equal evi1.Evd.evar_concl evi2.Evd.evar_concl &&
     Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
 
   let weak_progress glss gls =
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 20d075ae1..a633238f4 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Nameops
 open Term
+open Constr
 open Vars
 open Termops
 open Environ
@@ -284,12 +285,12 @@ let error_unsupported_deep_meta c =
     strbrk "supported; try \"refine\" instead.")
 
 let collect_meta_variables c =
-  let rec collrec deep acc c = match kind_of_term c with
+  let rec collrec deep acc c = match kind c with
     | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
     | Cast(c,_,_) -> collrec deep acc c
-    | (App _| Case _) -> Term.fold_constr (collrec deep) acc c
+    | (App _| Case _) -> Constr.fold (collrec deep) acc c
     | Proj (_, c) -> collrec deep acc c
-    | _ -> Term.fold_constr (collrec true) acc c
+    | _ -> Constr.fold (collrec true) acc c
   in
   List.rev (collrec false [] c)
 
@@ -332,7 +333,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
         (goalacc,t'ty,sigma,trm)
     else
-      match kind_of_term trm with
+      match kind trm with
       | Meta _ ->
 	let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in
 	  if !check && occur_meta sigma conclty then
@@ -372,7 +373,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	in
 	let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
         let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
-        let ans = if applicand == f && args == l then trm else Term.mkApp (applicand, args) in
+        let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
         (acc'',conclty',sigma, ans)
 
       | Proj (p,c) ->
@@ -394,7 +395,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
         let lf' = Array.rev_of_list rbranches in
         let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
-          else Term.mkCase (ci,p',c',lf')
+          else mkCase (ci,p',c',lf')
         in
 	(acc'',conclty',sigma, ans)
 
@@ -413,7 +414,7 @@ and mk_hdgoals sigma goal goalacc trm =
   let hyps = Goal.V82.hyps sigma goal in
   let mk_goal hyps concl = 
     Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
-  match kind_of_term trm with
+  match kind trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
 	let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in
@@ -433,7 +434,7 @@ and mk_hdgoals sigma goal goalacc trm =
 	  else mk_hdgoals sigma goal goalacc f
 	in
 	let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
-        let ans = if applicand == f && args == l then trm else Term.mkApp (applicand, args) in
+        let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
 	(acc'',conclty',sigma, ans)
 
     | Case (ci,p,c,lf) ->
@@ -447,7 +448,7 @@ and mk_hdgoals sigma goal goalacc trm =
 	let lf' = Array.rev_of_list rbranches in
 	let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
-          else Term.mkCase (ci,p',c',lf')
+          else mkCase (ci,p',c',lf')
 	in
 	(acc'',conclty',sigma, ans)
 
@@ -468,12 +469,12 @@ and mk_arggoals sigma goal goalacc funty allargs =
   let foldmap (goalacc, funty, sigma) harg =
     let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in
     let t = EConstr.Unsafe.to_constr t in
-    let rec collapse t = match kind_of_term t with
+    let rec collapse t = match kind t with
     | LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
     | _ -> t
     in
     let t = collapse t in
-    match kind_of_term t with
+    match kind t with
     | Prod (_, c1, b) ->
       let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in
       (acc, subst1 harg b, sigma), arg
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 9d0756b33..7df7fd66b 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -9,7 +9,7 @@
 (** Legacy proof engine. Do not use in newly written code. *)
 
 open Names
-open Term
+open Constr
 open Evd
 open Proof_type
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index adfe33786..21a65f8eb 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -9,7 +9,7 @@
 (** Global proof state. A quite redundant wrapper on {!Proof_global}. *)
 
 open Names
-open Term
+open Constr
 open Environ
 open Decl_kinds
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 621178982..97faa1684 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -320,7 +320,7 @@ let constrain_variables init uctx =
   let levels = Univ.Instance.levels (Univ.UContext.instance init) in
   UState.constrain_variables levels uctx
 
-type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
+type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * Evd.evar_universe_context
 
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 8c0f6ad85..6309f681f 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -86,7 +86,7 @@ val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
  * Both access the current proof state. The former is supposed to be
  * chained with a computation that completed the proof *)
 
-type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
+type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * Evd.evar_universe_context
 
 (* If allow_partial is set (default no) then an incomplete proof
  * is allowed (no error), and a warn is given if the proof is complete. *)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 2ad5f607f..20293cb9b 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -9,7 +9,7 @@
 (** Legacy proof engine. Do not use in newly written code. *)
 
 open Evd
-open Term
+open Constr
 
 (** This module defines the structure of proof tree and the tactic type. So, it
    is used by [Proof_tree] and [Refiner] *)
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index ccc2440a2..43e598773 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -9,7 +9,7 @@
 (** Interpretation layer of redexprs such as hnf, cbv, etc. *)
 
 open Names
-open Term
+open Constr
 open EConstr
 open Pattern
 open Genredexpr
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 3b0a9e5b6..cfdcde36e 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -17,7 +17,7 @@ open Proofview
 
 (** Printer used to print the constr which refine refines. *)
 val pr_constr :
-  (Environ.env -> Evd.evar_map -> Term.constr -> Pp.t) Hook.t
+  (Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t) Hook.t
 
 (** {7 Refinement primitives} *)
 
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 3ff010fe3..9c8777c41 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -37,7 +37,7 @@ val tclIDTAC_MESSAGE  : Pp.t -> tactic
 val tclEVARS : evar_map -> tactic
 val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
 
-val tclPUSHCONTEXT : Evd.rigid -> Univ.universe_context_set -> tactic -> tactic
+val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic
 val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
 
 val tclPUSHCONSTRAINTS : Univ.constraints -> tactic
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index de9f8e700..6441cfd19 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open EConstr
 open Evd