[api] Deprecate Term destructors, move to Constr

We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.

This is a step towards having a single module for `Constr`.

1 files changed, 6 insertions, 7 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index bcfbc8081e..afdceae061 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -9,7 +9,6 @@
 open CErrors
 open Util
 open Names
-open Term
 open Constr
 open Context
 open Evd
@@ -55,7 +54,7 @@ struct
   type t = Sorts.t
   let make s = s
   let kind sigma = function
-  | Type u -> sort_of_univ (Evd.normalize_universe sigma u)
+  | Sorts.Type u -> Sorts.sort_of_univ (Evd.normalize_universe sigma u)
   | s -> s
   let unsafe_to_sorts s = s
 end
@@ -85,16 +84,16 @@ let rec whd_evar sigma c =
     | Some c -> whd_evar sigma c
     | None -> c
     end
-  | App (f, args) when Term.isEvar f ->
+  | App (f, args) when isEvar f ->
     (** Enforce smart constructor invariant on applications *)
-    let ev = Term.destEvar f in
+    let ev = destEvar f in
     begin match safe_evar_value sigma ev with
     | None -> c
     | Some f -> whd_evar sigma (mkApp (f, args))
     end
-  | Cast (c0, k, t) when Term.isEvar c0 ->
+  | Cast (c0, k, t) when isEvar c0 ->
     (** Enforce smart constructor invariant on casts. *)
-    let ev = Term.destEvar c0 in
+    let ev = destEvar c0 in
     begin match safe_evar_value sigma ev with
     | None -> c
     | Some c -> whd_evar sigma (mkCast (c, k, t))
@@ -115,7 +114,7 @@ let rec to_constr sigma c = match Constr.kind c with
   | Some c -> to_constr sigma c
   | None -> Constr.map (fun c -> to_constr sigma c) c
   end
-| Sort (Type u) ->
+| Sort (Sorts.Type u) ->
   let u' = Evd.normalize_universe sigma u in
   if u' == u then c else mkSort (Sorts.sort_of_univ u')
 | Const (c', u) when not (Univ.Instance.is_empty u) ->