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

16 files changed, 71 insertions, 53 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 7f98ed427..c2bc8c079 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Constr
+
 let contrib_name = "btauto"
 
 let init_constant dir s =
@@ -106,7 +118,7 @@ module Bool = struct
     let negb = Lazy.force negb in
 
     let rec aux c = match decomp_term sigma c with
-    | Term.App (head, args) ->
+    | App (head, args) ->
       if head === andb && Array.length args = 2 then
         Andb (aux args.(0), aux args.(1))
       else if head === orb && Array.length args = 2 then
@@ -116,9 +128,9 @@ module Bool = struct
       else if head === negb && Array.length args = 1 then
         Negb (aux args.(0))
       else Var (Env.add env c)
-    | Term.Case (info, r, arg, pats) ->
+    | Case (info, r, arg, pats) ->
       let is_bool =
-        let i = info.Term.ci_ind in
+        let i = info.ci_ind in
         Names.eq_ind i (Lazy.force ind)
       in
       if is_bool then
@@ -176,9 +188,9 @@ module Btauto = struct
     let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in
     let var = EConstr.Unsafe.to_constr var in
     let rec to_list l = match decomp_term (Tacmach.project gl) l with
-    | Term.App (c, _)
+    | App (c, _)
       when c === (Lazy.force CoqList._nil) -> []
-    | Term.App (c, [|_; h; t|])
+    | App (c, [|_; h; t|])
       when c === (Lazy.force CoqList._cons) ->
       if h === (Lazy.force Bool.trueb) then (true :: to_list t)
       else if h === (Lazy.force Bool.falseb) then (false :: to_list t)
@@ -218,7 +230,7 @@ module Btauto = struct
       let concl = EConstr.Unsafe.to_constr concl in
       let t = decomp_term (Tacmach.New.project gl) concl in
       match t with
-      | Term.App (c, [|typ; p; _|]) when c === eq ->
+      | App (c, [|typ; p; _|]) when c === eq ->
       (* should be an equality [@eq poly ?p (Cst false)] *)
           let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in
           tac
@@ -236,7 +248,7 @@ module Btauto = struct
       let bool = Lazy.force Bool.typ in
       let t = decomp_term sigma concl in
       match t with
-      | Term.App (c, [|typ; tl; tr|])
+      | App (c, [|typ; tl; tr|])
           when typ === bool && c === eq ->
           let env = Env.empty () in
           let fl = Bool.quote env sigma tl in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index b869c04a2..06f56d06e 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 open Util
-open Term
+open Constr
 open EConstr
 open Vars
 open Termops
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index ae238b846..bb1587507 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,4 +1,5 @@
 open Pp
+open Constr
 open Glob_term
 open CErrors
 open Util
@@ -16,7 +17,7 @@ let mkGApp(rt,rtl)      = DAst.make @@ GApp(rt,rtl)
 let mkGLambda(n,t,b)    = DAst.make @@ GLambda(n,Explicit,t,b)
 let mkGProd(n,t,b)      = DAst.make @@ GProd(n,Explicit,t,b)
 let mkGLetIn(n,b,t,c)   = DAst.make @@ GLetIn(n,b,t,c)
-let mkGCases(rto,l,brl) = DAst.make @@ GCases(Term.RegularStyle,rto,l,brl)
+let mkGCases(rto,l,brl) = DAst.make @@ GCases(RegularStyle,rto,l,brl)
 let mkGHole ()          = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
 
 (*
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b0c9ff8fc..c6faa142a 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -109,7 +109,7 @@ let const_of_id id =
 
 let def_of_const t =
    match Constr.kind t with
-    Term.Const sp ->
+    Const sp ->
       (try (match Environ.constant_opt_value_in (Global.env()) sp with
              | Some c -> c
 	     | _ -> assert false)
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 5463893ad..ea8dcf57d 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -10,7 +10,7 @@
 
 open Util
 open Names
-open Term
+open Constr
 open CErrors
 open Evar_refiner
 open Tacmach
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 17011f206..c5254b37c 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Pp
+open Constr
 open Genarg
 open Stdarg
 open Tacarg
@@ -286,7 +287,6 @@ END
 (**********************************************************************)
 (* Hint Resolve                                                       *)
 
-open Term
 open EConstr
 open Vars
 open Coqlib
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 07047d016..642e52155 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Pp
+open Constr
 open Genarg
 open Stdarg
 open Pcoq.Prim
@@ -169,7 +170,7 @@ END
 
 
 TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ]
+| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ]
 END
 
 let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index a51c09ca4..8eeb8903e 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Term
+open Constr
 open EConstr
 open Hipattern
 open Names
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 4c0357dd8..c7abd58b0 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -19,10 +19,10 @@
 (************************************************************************)
 
 open Pp
-open Mutils
-open Goptions
 open Names
 open Constr
+open Goptions
+open Mutils
 
 (**
   * Debug flag 
@@ -601,10 +601,10 @@ struct
 
   let get_left_construct sigma term =
    match EConstr.kind sigma term with
-    | Term.Construct((_,i),_) -> (i,[| |])
-    | Term.App(l,rst) ->
+    | Construct((_,i),_) -> (i,[| |])
+    | App(l,rst) ->
        (match EConstr.kind sigma l with
-        | Term.Construct((_,i),_) -> (i,rst)
+        | Construct((_,i),_) -> (i,rst)
         |   _     -> raise ParseError
        )
     | _ ->   raise ParseError
@@ -688,7 +688,7 @@ struct
 
   let parse_q sigma term =
      match EConstr.kind sigma term with
-       | Term.App(c, args) -> if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then
+       | App(c, args) -> if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then
              {Mc.qnum = parse_z sigma args.(0) ; Mc.qden = parse_positive sigma args.(1) }
        else raise ParseError
    |  _ -> raise ParseError
@@ -904,8 +904,8 @@ struct
   let parse_zop gl (op,args) =
     let sigma = gl.sigma in
     match EConstr.kind sigma op with
-    | Term.Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1))
-    | Term.Ind((n,0),_) ->
+    | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1))
+    | Ind((n,0),_) ->
         if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_Z)
         then (Mc.OpEq, args.(1), args.(2))
         else raise ParseError
@@ -914,8 +914,8 @@ struct
   let parse_rop gl (op,args) =
     let sigma = gl.sigma in
     match EConstr.kind sigma op with
-     | Term.Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1))
-     | Term.Ind((n,0),_) ->
+     | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1))
+     | Ind((n,0),_) ->
         if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_R)
         then (Mc.OpEq, args.(1), args.(2))
         else raise ParseError
@@ -926,7 +926,7 @@ struct
 
   let is_constant sigma t = (* This is an approx *)
    match EConstr.kind sigma t with
-    | Term.Construct(i,_) -> true
+    | Construct(i,_) -> true
     |   _ -> false
 
   type 'a op =
@@ -1011,10 +1011,10 @@ struct
        try (Mc.PEc (parse_constant term) , env)
        with ParseError -> 
 	 match EConstr.kind sigma term with
-	   | Term.App(t,args) ->
+           | App(t,args) ->
                (
 		 match EConstr.kind sigma t with
-		   | Term.Const c ->
+                   | Const c ->
 		       ( match assoc_ops sigma t ops_spec  with
 			   | Binop f -> combine env f (args.(0),args.(1))
                    | Opp     -> let (expr,env) = parse_expr env args.(0) in
@@ -1077,13 +1077,13 @@ struct
 
   let rec rconstant sigma term =
    match EConstr.kind sigma term with
-    | Term.Const x ->
+    | Const x ->
         if EConstr.eq_constr sigma term (Lazy.force coq_R0)
         then Mc.C0
         else if EConstr.eq_constr sigma term (Lazy.force coq_R1)
         then Mc.C1
         else raise ParseError
-    | Term.App(op,args) -> 
+    | App(op,args) ->
 	begin
 	  try
             (* the evaluation order is important in the following *)
@@ -1153,7 +1153,7 @@ struct
     if debug
     then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ());
     match EConstr.kind sigma cstr with
-    | Term.App(op,args) ->
+    | App(op,args) ->
        let (op,lhs,rhs) = parse_op gl (op,args) in
        let (e1,env) = parse_expr sigma env lhs in
        let (e2,env) = parse_expr sigma env rhs in
@@ -1208,7 +1208,7 @@ struct
      
     let rec xparse_formula env tg term =
       match EConstr.kind sigma term with
-      | Term.App(l,rst) ->
+      | App(l,rst) ->
         (match rst with
         | [|a;b|] when EConstr.eq_constr sigma l (Lazy.force coq_and) ->
           let f,env,tg = xparse_formula env tg a in
@@ -1225,7 +1225,7 @@ struct
           let g,env,tg = xparse_formula env tg b in
           mkformula_binary mkIff term f g,env,tg
         | _ -> parse_atom env tg term)
-      | Term.Prod(typ,a,b) when EConstr.Vars.noccurn sigma 1 b ->
+      | Prod(typ,a,b) when EConstr.Vars.noccurn sigma 1 b ->
         let f,env,tg = xparse_formula env tg a in
         let g,env,tg = xparse_formula env tg b in
         mkformula_binary mkI term f g,env,tg
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 3594c8765..c615cf278 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -18,8 +18,8 @@
 open CErrors
 open Util
 open Names
+open Constr
 open Nameops
-open Term
 open EConstr
 open Tacticals.New
 open Tacmach.New
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index d18249784..e60348065 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Util
+open Constr
 open Const_omega
 module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -1036,13 +1037,13 @@ let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list =
   let decompose_tactic = decompose_tree env context solution_tree in
 
   Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >>
-  Tactics.convert_concl_no_check reified Term.DEFAULTcast >>
+  Tactics.convert_concl_no_check reified DEFAULTcast >>
   Tactics.apply (app coq_do_omega [|decompose_tactic|]) >>
   show_goal >>
   (if unsafe then
      (* Trust the produced term. Faster, but might fail later at Qed.
         Also handy when debugging, e.g. via a Show Proof after romega. *)
-     Tactics.convert_concl_no_check (Lazy.force coq_True) Term.VMcast
+     Tactics.convert_concl_no_check (Lazy.force coq_True) VMcast
    else
      Tactics.normalise_vm_in_concl) >>
   Tactics.apply (Lazy.force coq_I)
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 =