[api] Remove deprecated object from `Term`

We remove most of what was deprecated in `Term`. Now, `intf` and
`kernel` are almost deprecation-free, tho I am not very convinced
about the whole `Term -> Constr` renaming but I'm afraid there is no
way back.

Inconsistencies with the constructor policy (see #6440) remain along
the code-base and I'm afraid I don't see a plan to reconcile them.

The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a
good idea as someone added a `List` module inside it.

5 files changed, 21 insertions, 18 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index c0026616d..3f6503e73 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -423,12 +423,12 @@ let mk_anon_id t gl_ids =
     (set s i (Char.chr (Char.code (get s i) + 1)); s) in
   Id.of_bytes (loop (n - 1))
 
-let convert_concl_no_check t = Tactics.convert_concl_no_check t Term.DEFAULTcast
-let convert_concl t = Tactics.convert_concl t Term.DEFAULTcast
+let convert_concl_no_check t = Tactics.convert_concl_no_check t DEFAULTcast
+let convert_concl t = Tactics.convert_concl t DEFAULTcast
 
 let rename_hd_prod orig_name_ref gl =
   match EConstr.kind (project gl) (pf_concl gl) with
-  | Term.Prod(_,src,tgt) ->
+  | Prod(_,src,tgt) ->
       Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkProd (!orig_name_ref,src,tgt))) gl
   | _ -> CErrors.anomaly (str "gentac creates no product")
 
@@ -1446,7 +1446,7 @@ let tclINTRO_ANON = tclINTRO ~id:None ~conclusion:return
 
 let tclRENAME_HD_PROD name = Goal.enter begin fun gl ->
   let convert_concl_no_check t =
-    Tactics.convert_concl_no_check t Term.DEFAULTcast in
+    Tactics.convert_concl_no_check t DEFAULTcast in
   let concl = Goal.concl gl in
   let sigma = Goal.sigma gl in
   match EConstr.kind sigma concl with
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 87d107d65..83b4d6562 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -14,6 +14,7 @@ open Util
 open Names
 open Printer
 open Term
+open Constr
 open Termops
 open Globnames
 open Misctypes
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index b397c5531..8207bc11e 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -12,6 +12,7 @@ open Ssrmatching_plugin
 
 open Util
 open Names
+open Constr
 
 open Proofview
 open Proofview.Notations
@@ -90,11 +91,11 @@ open State
 (** Warning: unlike [nb_deps_assums], it does not perform reduction *)
 let rec nb_assums cur env sigma t =
   match EConstr.kind sigma t with
-  | Term.Prod(name,ty,body) ->
+  | Prod(name,ty,body) ->
      nb_assums (cur+1) env sigma body
-  | Term.LetIn(name,ty,t1,t2) ->
+  | LetIn(name,ty,t1,t2) ->
     nb_assums (cur+1) env sigma t2
-  | Term.Cast(t,_,_) ->
+  | Cast(t,_,_) ->
      nb_assums cur env sigma t
   | _ -> cur
 let nb_assums = nb_assums 0
@@ -556,7 +557,7 @@ let rec eqmoveipats eqpat = function
 let ssrsmovetac = Goal.enter begin fun g ->
   let sigma, concl = Goal.(sigma g, concl g) in
   match EConstr.kind sigma concl with
-  | Term.Prod _ | Term.LetIn _ -> tclUNIT ()
+  | Prod _ | LetIn _ -> tclUNIT ()
   | _ -> Tactics.hnf_in_concl
 end
 
@@ -594,8 +595,8 @@ let rec is_Evar_or_CastedMeta sigma x =
 
 let occur_existential_or_casted_meta sigma c =
   let rec occrec c = match EConstr.kind sigma c with
-    | Term.Evar _ -> raise Not_found
-    | Term.Cast (m,_,_) when EConstr.isMeta sigma m -> raise Not_found
+    | Evar _ -> raise Not_found
+    | Cast (m,_,_) when EConstr.isMeta sigma m -> raise Not_found
     | _ -> EConstr.iter sigma occrec c
   in
   try occrec c; false
@@ -625,7 +626,7 @@ let tacFIND_ABSTRACT_PROOF check_lock abstract_n =
     let sigma, env = Goal.(sigma g, env g) in
     let l = Evd.fold_undefined (fun e ei l ->
       match EConstr.kind sigma ei.Evd.evar_concl with
-      | Term.App(hd, [|ty; n; lock|])
+      | App(hd, [|ty; n; lock|])
         when (not check_lock ||
                    (occur_existential_or_casted_meta sigma ty &&
                     is_Evar_or_CastedMeta sigma lock)) &&
@@ -654,8 +655,8 @@ let ssrabstract dgens =
       let sigma, env, concl = Goal.(sigma g, env g, concl g) in
       let t = args_id.(0) in
       match EConstr.kind sigma t with
-      | (Term.Evar _ | Term.Meta _) -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id
-      | Term.Cast(m,_,_)
+      | (Evar _ | Meta _) -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id
+      | Cast(m,_,_)
         when EConstr.isEvar sigma m || EConstr.isMeta sigma m ->
           Ssrcommon.tacUNIFY concl t <*> tclUNIT id
       | _ ->
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 5f3967440..138b42e54 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -10,6 +10,7 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
+let _vmcast = Constr.VMcast
 open Names
 open Pp
 open Pcoq
@@ -17,7 +18,6 @@ open Ltac_plugin
 open Genarg
 open Stdarg
 open Tacarg
-open Term
 open Libnames
 open Tactics
 open Tacmach
@@ -1938,7 +1938,7 @@ END
 
 let vmexacttac pf =
   Goal.nf_enter begin fun gl ->
-  exact_no_check (EConstr.mkCast (pf, VMcast, Tacmach.New.pf_concl gl))
+  exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl))
   end
 
 TACTIC EXTEND ssrexact
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 937e68b06..372ae86bd 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -11,6 +11,7 @@
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
 open Names
+open Constr
 open Termops
 open Tacmach
 open Misctypes
@@ -103,10 +104,10 @@ let endclausestac id_map clseq gl_id cl0 gl =
   | ids, dc' ->
     forced && ids = [] && (not hide_goal || dc' = [] && c_hidden) in
   let rec unmark c = match EConstr.kind (project gl) c with
-  | Term.Var id when hidden_clseq clseq && id = gl_id -> cl0
-  | Term.Prod (Name id, t, c') when List.mem_assoc id id_map ->
+  | Var id when hidden_clseq clseq && id = gl_id -> cl0
+  | Prod (Name id, t, c') when List.mem_assoc id id_map ->
     EConstr.mkProd (Name (orig_id id), unmark t, unmark c')
-  | Term.LetIn (Name id, v, t, c') when List.mem_assoc id id_map ->
+  | LetIn (Name id, v, t, c') when List.mem_assoc id id_map ->
     EConstr.mkLetIn (Name (orig_id id), unmark v, unmark t, unmark c')
   | _ -> EConstr.map (project gl) unmark c in
   let utac hyp =