[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`.

4 files changed, 12 insertions, 13 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) ->
diff --git a/engine/evd.ml b/engine/evd.ml
index 8d465384b1..60bd6de2ae 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -243,7 +243,7 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) 0
 
 let make_evar_instance_array info args =
-  evar_instance_array (NamedDecl.get_id %> Term.isVarId) info args
+  evar_instance_array (NamedDecl.get_id %> isVarId) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -707,10 +707,10 @@ let extract_all_conv_pbs evd =
   extract_conv_pbs evd (fun _ -> true)
 
 let loc_of_conv_pb evd (pbty,env,t1,t2) =
-  match kind (fst (Term.decompose_app t1)) with
+  match kind (fst (decompose_app t1)) with
   | Evar (evk1,_) -> fst (evar_source evk1 evd)
   | _ ->
-  match kind (fst (Term.decompose_app t2)) with
+  match kind (fst (decompose_app t2)) with
   | Evar (evk2,_) -> fst (evar_source evk2 evd)
   | _             -> None
 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 598358c472..3b945c87f9 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1200,7 +1200,7 @@ module V82 = struct
    { Evd.it = comb ; sigma = solution }
 
   let top_goals initial { solution=solution; } =
-    let goals = CList.map (fun (t,_) -> fst (Term.destEvar (EConstr.Unsafe.to_constr t))) initial in
+    let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
     { Evd.it = goals ; sigma=solution; }
 
   let top_evars initial =
diff --git a/engine/univops.ml b/engine/univops.ml
index 9dc138eb8d..d498b2e0d8 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -6,8 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Constr
 open Univ
+open Constr
 
 let universes_of_constr c =
   let rec aux s c = 
@@ -15,7 +15,7 @@ let universes_of_constr c =
     | Const (_, u) | Ind (_, u) | Construct (_, u) ->
       LSet.fold LSet.add (Instance.levels u) s
     | Sort u when not (Sorts.is_small u) -> 
-      let u = Term.univ_of_sort u in
+      let u = Sorts.univ_of_sort u in
       LSet.fold LSet.add (Universe.levels u) s
     | _ -> Constr.fold aux s c
   in aux LSet.empty c