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

13 files changed, 14 insertions, 11 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 8f50b0aa2..aca7f6c65 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 open Util
-open Term
+open Constr
 open EConstr
 open Names
 open Pattern
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 3e08c6d87..28eaf9f28 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -18,6 +18,7 @@ open CErrors
 open Util
 open Names
 open Term
+open Constr
 open Termops
 open EConstr
 open Tacmach
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c285f21e7..b92bc75bc 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Term
+open Constr
 open EConstr
 open Hipattern
 open Tactics
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 3df9e3f82..80d07c5c0 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -12,7 +12,7 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
+open Constr
 open Termops
 open EConstr
 open Proof_type
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index b0deeed17..176701d99 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -17,7 +17,7 @@
 open Util
 open Names
 open Namegen
-open Term
+open Constr
 open EConstr
 open Declarations
 open Tactics
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8904cd170..f9e06391a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -15,6 +15,7 @@ open Util
 open Names
 open Nameops
 open Term
+open Constr
 open Termops
 open EConstr
 open Vars
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 7b5be4c1c..7b943b373 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -12,7 +12,7 @@ open Pp
 open Util
 open CErrors
 open Names
-open Term
+open Constr
 open Evd
 open EConstr
 open Vars
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index b8f1ed720..5d264058a 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -12,7 +12,7 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
+open Constr
 open Termops
 open EConstr
 open Inductiveops
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b346ed223..28cfd57a2 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -14,6 +14,7 @@ open Util
 open Names
 open Term
 open Termops
+open Constr
 open EConstr
 open Vars
 open Namegen
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index a4cdc1592..f47e6b2cd 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -12,9 +12,9 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
 open Termops
 open Environ
+open Constr
 open EConstr
 open Vars
 open Namegen
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6c7db26c7..732d06f8a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -509,7 +509,7 @@ module New = struct
       match Evd.evar_body evi with
       | Evd.Evar_empty -> Some (evk,evi)
       | Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with
-        | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
+        | Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
         | _ -> 
           (* We make the assumption that there is no way to refine an
             evar remaining after typing from the initial term given to
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bb57e2bf4..58c62af85 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1910,8 +1910,8 @@ let cast_no_check cast c =
     exact_no_check (mkCast (c, cast, concl))
   end
 
-let vm_cast_no_check c = cast_no_check Term.VMcast c
-let native_cast_no_check c = cast_no_check Term.NATIVEcast c
+let vm_cast_no_check c = cast_no_check VMcast c
+let native_cast_no_check c = cast_no_check NATIVEcast c
 
 let exact_proof c =
   let open Tacmach.New in
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 611799990..8bdcc6321 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -290,7 +290,7 @@ struct
     | Const (c,u)    -> Term (DRef (ConstRef c))
     | Ind (i,u)      -> Term (DRef (IndRef i))
     | Construct (c,u)-> Term (DRef (ConstructRef c))
-    | Term.Meta _    -> assert false
+    | Meta _         -> assert false
     | Evar (i,_)     ->
       let meta =
         try Evar.Map.find i !metas