[api] Move structures deprecated in the API to the core.

We do up to `Term` which is the main bulk of the changes.

3 files changed, 140 insertions, 138 deletions

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index c27ac2ea4..5397b0065 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -7,14 +7,16 @@
  *************************************************************************)
 
 open Names
+open Term
+open Constr
 
 let module_refl_name = "ReflOmegaCore"
 let module_refl_path = ["Coq"; "romega"; module_refl_name]
 
 type result =
   | Kvar of string
-  | Kapp of string * Term.constr list
-  | Kimp of Term.constr * Term.constr
+  | Kapp of string * constr list
+  | Kimp of constr * constr
   | Kufo
 
 let meaningful_submodule = [ "Z"; "N"; "Pos" ]
@@ -30,27 +32,27 @@ let string_of_global r =
   prefix^(Names.Id.to_string (Nametab.basename_of_global r))
 
 let destructurate t =
-  let c, args = Term.decompose_app t in
-  match Term.kind_of_term c, args with
-  | Term.Const (sp,_), args ->
+  let c, args = decompose_app t in
+  match Constr.kind c, args with
+  | Const (sp,_), args ->
      Kapp (string_of_global (Globnames.ConstRef sp), args)
-  | Term.Construct (csp,_) , args ->
+  | Construct (csp,_) , args ->
      Kapp (string_of_global (Globnames.ConstructRef csp), args)
-  | Term.Ind (isp,_), args ->
+  | Ind (isp,_), args ->
      Kapp (string_of_global (Globnames.IndRef isp), args)
-  | Term.Var id, [] -> Kvar(Names.Id.to_string id)
-  | Term.Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
+  | Var id, [] -> Kvar(Names.Id.to_string id)
+  | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
   | _ -> Kufo
 
 exception DestConstApp
 
 let dest_const_apply t =
-  let f,args = Term.decompose_app t in
+  let f,args = decompose_app t in
   let ref =
-  match Term.kind_of_term f with
-    | Term.Const (sp,_)      -> Globnames.ConstRef sp
-    | Term.Construct (csp,_) -> Globnames.ConstructRef csp
-    | Term.Ind (isp,_)       -> Globnames.IndRef isp
+  match Constr.kind f with
+    | Const (sp,_)      -> Globnames.ConstRef sp
+    | Construct (csp,_) -> Globnames.ConstructRef csp
+    | Ind (isp,_)       -> Globnames.IndRef isp
     | _ -> raise DestConstApp
   in Nametab.basename_of_global ref, args
 
@@ -129,7 +131,7 @@ let coq_O = lazy(init_constant "O")
 
 let rec mk_nat = function
   | 0 -> Lazy.force coq_O
-  | n -> Term.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |])
+  | n -> mkApp (Lazy.force coq_S, [| mk_nat (n-1) |])
 
 (* Lists *)
 
@@ -141,47 +143,47 @@ let mkListConst c =
     if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|]
     else fun _ -> Univ.Instance.empty
   in
-    fun u -> Term.mkConstructU (Globnames.destConstructRef r, inst u)
+    fun u -> mkConstructU (Globnames.destConstructRef r, inst u)
 
-let coq_cons univ typ = Term.mkApp (mkListConst "cons" univ, [|typ|])
-let coq_nil univ typ =  Term.mkApp (mkListConst "nil" univ, [|typ|])
+let coq_cons univ typ = mkApp (mkListConst "cons" univ, [|typ|])
+let coq_nil univ typ =  mkApp (mkListConst "nil" univ, [|typ|])
 
 let mk_list univ typ l =
   let rec loop = function
     | [] -> coq_nil univ typ
     | (step :: l) ->
-	Term.mkApp (coq_cons univ typ, [| step; loop l |]) in
+	mkApp (coq_cons univ typ, [| step; loop l |]) in
   loop l
 
 let mk_plist = 
   let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in
-    fun l -> mk_list type1lev Term.mkProp l
+    fun l -> mk_list type1lev mkProp l
 
 let mk_list = mk_list Univ.Level.set
 
 type parse_term =
-  | Tplus of Term.constr * Term.constr
-  | Tmult of Term.constr * Term.constr
-  | Tminus of Term.constr * Term.constr
-  | Topp of Term.constr
-  | Tsucc of Term.constr
+  | Tplus of constr * constr
+  | Tmult of constr * constr
+  | Tminus of constr * constr
+  | Topp of constr
+  | Tsucc of constr
   | Tnum of Bigint.bigint
   | Tother
 
 type parse_rel =
-  | Req of Term.constr * Term.constr
-  | Rne of Term.constr * Term.constr
-  | Rlt of Term.constr * Term.constr
-  | Rle of Term.constr * Term.constr
-  | Rgt of Term.constr * Term.constr
-  | Rge of Term.constr * Term.constr
+  | Req of constr * constr
+  | Rne of constr * constr
+  | Rlt of constr * constr
+  | Rle of constr * constr
+  | Rgt of constr * constr
+  | Rge of constr * constr
   | Rtrue
   | Rfalse
-  | Rnot of Term.constr
-  | Ror of Term.constr * Term.constr
-  | Rand of Term.constr * Term.constr
-  | Rimp of Term.constr * Term.constr
-  | Riff of Term.constr * Term.constr
+  | Rnot of constr
+  | Ror of constr * constr
+  | Rand of constr * constr
+  | Rimp of constr * constr
+  | Riff of constr * constr
   | Rother
 
 let parse_logic_rel c = match destructurate c with
@@ -209,29 +211,29 @@ let rec mk_positive n =
   if Bigint.equal n Bigint.one then Lazy.force coq_xH
   else
     let (q,r) = Bigint.euclid n Bigint.two in
-    Term.mkApp
+    mkApp
       ((if Bigint.equal r Bigint.zero
         then Lazy.force coq_xO else Lazy.force coq_xI),
        [| mk_positive q |])
 
 let mk_N = function
   | 0 -> Lazy.force coq_N0
-  | n -> Term.mkApp (Lazy.force coq_Npos,
+  | n -> mkApp (Lazy.force coq_Npos,
                      [| mk_positive (Bigint.of_int n) |])
 
 module type Int = sig
-  val typ : Term.constr Lazy.t
-  val is_int_typ : [ `NF ] Proofview.Goal.t -> Term.constr -> bool
-  val plus : Term.constr Lazy.t
-  val mult : Term.constr Lazy.t
-  val opp : Term.constr Lazy.t
-  val minus : Term.constr Lazy.t
-
-  val mk : Bigint.bigint -> Term.constr
-  val parse_term : Term.constr -> parse_term
-  val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel
+  val typ : constr Lazy.t
+  val is_int_typ : [ `NF ] Proofview.Goal.t -> constr -> bool
+  val plus : constr Lazy.t
+  val mult : constr Lazy.t
+  val opp : constr Lazy.t
+  val minus : constr Lazy.t
+
+  val mk : Bigint.bigint -> constr
+  val parse_term : constr -> parse_term
+  val parse_rel : [ `NF ] Proofview.Goal.t -> constr -> parse_rel
   (* check whether t is built only with numbers and + * - *)
-  val get_scalar : Term.constr -> Bigint.bigint option
+  val get_scalar : constr -> Bigint.bigint option
 end
 
 module Z : Int = struct
@@ -266,9 +268,9 @@ let recognize_Z t =
 let mk_Z n =
   if Bigint.equal n Bigint.zero then Lazy.force coq_Z0
   else if Bigint.is_strictly_pos n then
-    Term.mkApp (Lazy.force coq_Zpos, [| mk_positive n |])
+    mkApp (Lazy.force coq_Zpos, [| mk_positive n |])
   else
-    Term.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |])
+    mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |])
 
 let mk = mk_Z
 
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index 80e00e4e1..5ba063d9d 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -8,116 +8,117 @@
 
 
 (** Coq objects used in romega *)
+open Constr
 
 (* from Logic *)
-val coq_refl_equal : Term.constr lazy_t
-val coq_and : Term.constr lazy_t
-val coq_not : Term.constr lazy_t
-val coq_or : Term.constr lazy_t
-val coq_True : Term.constr lazy_t
-val coq_False : Term.constr lazy_t
-val coq_I : Term.constr lazy_t
+val coq_refl_equal : constr lazy_t
+val coq_and : constr lazy_t
+val coq_not : constr lazy_t
+val coq_or : constr lazy_t
+val coq_True : constr lazy_t
+val coq_False : constr lazy_t
+val coq_I : constr lazy_t
 
 (* from ReflOmegaCore/ZOmega *)
 
-val coq_t_int : Term.constr lazy_t
-val coq_t_plus : Term.constr lazy_t
-val coq_t_mult : Term.constr lazy_t
-val coq_t_opp : Term.constr lazy_t
-val coq_t_minus : Term.constr lazy_t
-val coq_t_var : Term.constr lazy_t
-
-val coq_proposition : Term.constr lazy_t
-val coq_p_eq : Term.constr lazy_t
-val coq_p_leq : Term.constr lazy_t
-val coq_p_geq : Term.constr lazy_t
-val coq_p_lt : Term.constr lazy_t
-val coq_p_gt : Term.constr lazy_t
-val coq_p_neq : Term.constr lazy_t
-val coq_p_true : Term.constr lazy_t
-val coq_p_false : Term.constr lazy_t
-val coq_p_not : Term.constr lazy_t
-val coq_p_or : Term.constr lazy_t
-val coq_p_and : Term.constr lazy_t
-val coq_p_imp : Term.constr lazy_t
-val coq_p_prop : Term.constr lazy_t
-
-val coq_s_bad_constant : Term.constr lazy_t
-val coq_s_divide : Term.constr lazy_t
-val coq_s_not_exact_divide : Term.constr lazy_t
-val coq_s_sum : Term.constr lazy_t
-val coq_s_merge_eq : Term.constr lazy_t
-val coq_s_split_ineq : Term.constr lazy_t
-
-val coq_direction : Term.constr lazy_t
-val coq_d_left : Term.constr lazy_t
-val coq_d_right : Term.constr lazy_t
-
-val coq_e_split : Term.constr lazy_t
-val coq_e_extract : Term.constr lazy_t
-val coq_e_solve : Term.constr lazy_t
-
-val coq_interp_sequent : Term.constr lazy_t
-val coq_do_omega : Term.constr lazy_t
-
-val mk_nat : int -> Term.constr
-val mk_N : int -> Term.constr
+val coq_t_int : constr lazy_t
+val coq_t_plus : constr lazy_t
+val coq_t_mult : constr lazy_t
+val coq_t_opp : constr lazy_t
+val coq_t_minus : constr lazy_t
+val coq_t_var : constr lazy_t
+
+val coq_proposition : constr lazy_t
+val coq_p_eq : constr lazy_t
+val coq_p_leq : constr lazy_t
+val coq_p_geq : constr lazy_t
+val coq_p_lt : constr lazy_t
+val coq_p_gt : constr lazy_t
+val coq_p_neq : constr lazy_t
+val coq_p_true : constr lazy_t
+val coq_p_false : constr lazy_t
+val coq_p_not : constr lazy_t
+val coq_p_or : constr lazy_t
+val coq_p_and : constr lazy_t
+val coq_p_imp : constr lazy_t
+val coq_p_prop : constr lazy_t
+
+val coq_s_bad_constant : constr lazy_t
+val coq_s_divide : constr lazy_t
+val coq_s_not_exact_divide : constr lazy_t
+val coq_s_sum : constr lazy_t
+val coq_s_merge_eq : constr lazy_t
+val coq_s_split_ineq : constr lazy_t
+
+val coq_direction : constr lazy_t
+val coq_d_left : constr lazy_t
+val coq_d_right : constr lazy_t
+
+val coq_e_split : constr lazy_t
+val coq_e_extract : constr lazy_t
+val coq_e_solve : constr lazy_t
+
+val coq_interp_sequent : constr lazy_t
+val coq_do_omega : constr lazy_t
+
+val mk_nat : int -> constr
+val mk_N : int -> constr
 
 (** Precondition: the type of the list is in Set *)
-val mk_list : Term.constr -> Term.constr list -> Term.constr
-val mk_plist : Term.types list -> Term.types
+val mk_list : constr -> constr list -> constr
+val mk_plist : types list -> types
 
 (** Analyzing a coq term *)
 
 (* The generic result shape of the analysis of a term.
    One-level depth, except when a number is found *)
 type parse_term =
-    Tplus of Term.constr * Term.constr
-  | Tmult of Term.constr * Term.constr
-  | Tminus of Term.constr * Term.constr
-  | Topp of Term.constr
-  | Tsucc of Term.constr
+    Tplus of constr * constr
+  | Tmult of constr * constr
+  | Tminus of constr * constr
+  | Topp of constr
+  | Tsucc of constr
   | Tnum of Bigint.bigint
   | Tother
 
 (* The generic result shape of the analysis of a relation.
    One-level depth. *)
 type parse_rel =
-    Req of Term.constr * Term.constr
-  | Rne of Term.constr * Term.constr
-  | Rlt of Term.constr * Term.constr
-  | Rle of Term.constr * Term.constr
-  | Rgt of Term.constr * Term.constr
-  | Rge of Term.constr * Term.constr
+    Req of constr * constr
+  | Rne of constr * constr
+  | Rlt of constr * constr
+  | Rle of constr * constr
+  | Rgt of constr * constr
+  | Rge of constr * constr
   | Rtrue
   | Rfalse
-  | Rnot of Term.constr
-  | Ror of Term.constr * Term.constr
-  | Rand of Term.constr * Term.constr
-  | Rimp of Term.constr * Term.constr
-  | Riff of Term.constr * Term.constr
+  | Rnot of constr
+  | Ror of constr * constr
+  | Rand of constr * constr
+  | Rimp of constr * constr
+  | Riff of constr * constr
   | Rother
 
 (* A module factorizing what we should now about the number representation *)
 module type Int =
   sig
     (* the coq type of the numbers *)
-    val typ : Term.constr Lazy.t
+    val typ : constr Lazy.t
     (* Is a constr expands to the type of these numbers *)
-    val is_int_typ : [ `NF ] Proofview.Goal.t -> Term.constr -> bool
+    val is_int_typ : [ `NF ] Proofview.Goal.t -> constr -> bool
     (* the operations on the numbers *)
-    val plus : Term.constr Lazy.t
-    val mult : Term.constr Lazy.t
-    val opp : Term.constr Lazy.t
-    val minus : Term.constr Lazy.t
+    val plus : constr Lazy.t
+    val mult : constr Lazy.t
+    val opp : constr Lazy.t
+    val minus : constr Lazy.t
     (* building a coq number *)
-    val mk : Bigint.bigint -> Term.constr
+    val mk : Bigint.bigint -> constr
     (* parsing a term (one level, except if a number is found) *)
-    val parse_term : Term.constr -> parse_term
+    val parse_term : constr -> parse_term
     (* parsing a relation expression, including = < <= >= > *)
-    val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel
+    val parse_rel : [ `NF ] Proofview.Goal.t -> constr -> parse_rel
     (* Is a particular term only made of numbers and + * - ? *)
-    val get_scalar : Term.constr -> Bigint.bigint option
+    val get_scalar : constr -> Bigint.bigint option
   end
 
 (* Currently, we only use Z numbers *)
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 661485aee..430b608f4 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
@@ -27,8 +28,6 @@ let pp i = print_int i; print_newline (); flush stdout
 (* More readable than the prefix notation *)
 let (>>) = Tacticals.New.tclTHEN
 
-let mkApp = Term.mkApp
-
 (* \section{Types}
   \subsection{How to walk in a term}
   To represent how to get to a proposition. Only choice points are
@@ -68,14 +67,14 @@ type comparaison = Eq | Leq | Geq | Gt | Lt | Neq
    (it could contains some [Term.Var] but no [Term.Rel]). So no need to
    lift when breaking or creating arrows. *)
 type oproposition =
-    Pequa of Term.constr * oequation (* constr = copy of the Coq formula *)
+    Pequa of constr * oequation (* constr = copy of the Coq formula *)
   | Ptrue
   | Pfalse
   | Pnot of oproposition
   | Por of int * oproposition * oproposition
   | Pand of int * oproposition * oproposition
   | Pimp of int * oproposition * oproposition
-  | Pprop of Term.constr
+  | Pprop of constr
 
 (* The equations *)
 and oequation = {
@@ -102,9 +101,9 @@ and oequation = {
 
 type environment = {
   (* La liste des termes non reifies constituant l'environnement global *)
-  mutable terms : Term.constr list;
+  mutable terms : constr list;
   (* La meme chose pour les propositions *)
-  mutable props : Term.constr list;
+  mutable props : constr list;
   (* Traduction des indices utilisés ici en les indices finaux utilisés par
    * la tactique Omega après dénombrement des variables utiles *)
   real_indices : int IntHtbl.t;
@@ -219,7 +218,7 @@ let display_omega_var i = Printf.sprintf "OV%d" i
    calcul des variables utiles. *)
 
 let add_reified_atom t env =
-  try List.index0 Term.eq_constr t env.terms
+  try List.index0 Constr.equal t env.terms
   with Not_found ->
     let i = List.length env.terms in
     env.terms <- env.terms @ [t]; i
@@ -237,7 +236,7 @@ let set_reified_atom v t env =
 (* \subsection{Gestion de l'environnement de proposition pour Omega} *)
 (* ajout d'une proposition *)
 let add_prop env t =
-  try List.index0 Term.eq_constr t env.props
+  try List.index0 Constr.equal t env.props
   with Not_found ->
     let i = List.length env.props in  env.props <- env.props @ [t]; i
 
@@ -560,7 +559,7 @@ let reify_hyp env gl i =
   | LocalDef (_,d,t) when Z.is_int_typ gl (EConstr.Unsafe.to_constr t) ->
      let d = EConstr.Unsafe.to_constr d in
      let dummy = Lazy.force coq_True in
-     let p = mk_equation env ctxt dummy Eq (Term.mkVar i) d in
+     let p = mk_equation env ctxt dummy Eq (mkVar i) d in
      i,Defined,p
   | LocalDef (_,_,t) | LocalAssum (_,t) ->
      let t = EConstr.Unsafe.to_constr t in
@@ -1012,7 +1011,7 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list =
       (fun id ->
         match Id.Map.find id reified_hyps with
         | Defined,p ->
-           reified_of_proposition env p, mk_refl (Term.mkVar id)
+           reified_of_proposition env p, mk_refl (mkVar id)
         | Assumed,p ->
            reified_of_proposition env (maximize_prop useful_equa_ids p),
            EConstr.mkVar id