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

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

54 files changed, 395 insertions, 404 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 6281b2675..da8955f0d 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -12,12 +12,12 @@ let get_inductive dir s =
   let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in
   Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ()))
 
-let decomp_term sigma (c : Term.constr) =
-  Term.kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c)))
+let decomp_term sigma (c : Constr.t) =
+  Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c)))
 
-let lapp c v  = Term.mkApp (Lazy.force c, v)
+let lapp c v  = Constr.mkApp (Lazy.force c, v)
 
-let (===) = Term.eq_constr
+let (===) = Constr.equal
 
 module CoqList = struct
   let path = ["Init"; "Datatypes"]
@@ -53,17 +53,11 @@ end
 
 module Env = struct
 
-  module ConstrHashed = struct
-    type t = Term.constr
-    let equal = Term.eq_constr
-    let hash = Term.hash_constr
-  end
-
-  module ConstrHashtbl = Hashtbl.Make (ConstrHashed)
+  module ConstrHashtbl = Hashtbl.Make (Constr)
 
   type t = (int ConstrHashtbl.t * int ref)
 
-  let add (tbl, off) (t : Term.constr) =
+  let add (tbl, off) (t : Constr.t) =
     try ConstrHashtbl.find tbl t 
     with
     | Not_found -> 
@@ -103,7 +97,7 @@ module Bool = struct
   | Negb of t
   | Ifb of t * t * t
 
-  let quote (env : Env.t) sigma (c : Term.constr) : t =
+  let quote (env : Env.t) sigma (c : Constr.t) : t =
     let trueb = Lazy.force trueb in
     let falseb = Lazy.force falseb in
     let andb = Lazy.force andb in
@@ -170,7 +164,7 @@ module Btauto = struct
   | Bool.Xorb (b1, b2) -> lapp f_xor [|convert b1; convert b2|]
   | Bool.Ifb (b1, b2, b3) -> lapp f_ifb [|convert b1; convert b2; convert b3|]
 
-  let convert_env env : Term.constr = 
+  let convert_env env : Constr.t = 
     CoqList.of_list (Lazy.force Bool.typ) env
 
   let reify env t = lapp eval [|convert_env env; convert t|]
@@ -249,7 +243,7 @@ module Btauto = struct
           let env = Env.to_list env in
           let fl = reify env fl in
           let fr = reify env fr in
-          let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
+          let changed_gl = Constr.mkApp (c, [|typ; fl; fr|]) in
           let changed_gl = EConstr.of_constr changed_gl in
           Tacticals.New.tclTHENLIST [
             Tactics.change_concl changed_gl;
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 182821322..faabd7c14 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -11,14 +11,15 @@
 (* Plus some e-matching and constructor handling by P. Corbineau *)
 
 open CErrors
-open Util
 open Pp
 open Goptions
 open Names
 open Term
+open Constr
 open Vars
 open Tacmach
 open Evd
+open Util
 
 let init_size=5
 
@@ -154,7 +155,7 @@ let rec term_equal t1 t2 =
 open Hashset.Combine
 
 let rec hash_term = function
-  | Symb c -> combine 1 (hash_constr c)
+  | Symb c -> combine 1 (Constr.hash c)
   | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2)
   | Eps i -> combine 3 (Id.hash i)
   | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2)
@@ -215,7 +216,7 @@ type representative=
      mutable lfathers:Int.Set.t;
      mutable fathers:Int.Set.t;
      mutable inductive_status: inductive_status;
-     class_type : Term.types;
+     class_type : types;
      mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *)
 
 type cl = Rep of representative| Eqto of int*equality
@@ -232,7 +233,7 @@ type node =
 module Constrhash = Hashtbl.Make
   (struct type t = constr
 	  let equal = eq_constr_nounivs
-	  let hash = hash_constr
+	  let hash = Constr.hash
    end)
 module Typehash = Constrhash
 
@@ -438,7 +439,7 @@ and applist_proj c l =
   | Symb s -> applist_projection s l
   | _ -> applistc (constr_of_term c) l
 and applist_projection c l =
-  match kind_of_term c with
+  match Constr.kind c with
   | Const c when Environ.is_projection (fst c) (Global.env()) ->
     let p = Projection.make (fst c) false in
     (match l with 
@@ -454,7 +455,7 @@ and applist_projection c l =
 let rec canonize_name sigma c =
   let c = EConstr.Unsafe.to_constr c in
   let func c = canonize_name sigma (EConstr.of_constr c) in
-    match kind_of_term c with
+    match Constr.kind c with
       | Const (kn,u) ->
 	  let canon_const = Constant.make1 (Constant.canonical kn) in 
 	    (mkConstU (canon_const,u))
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index f904aa3e6..23cd2161d 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Util
-open Term
+open Constr
 open Names
 
 type pa_constructor =
@@ -85,7 +85,7 @@ type representative=
      mutable lfathers:Int.Set.t;
      mutable fathers:Int.Set.t;
      mutable inductive_status: inductive_status;
-     class_type : Term.types;
+     class_type : types;
      mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *)
 
 type cl = Rep of representative| Eqto of int*equality
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index a43a167e8..97efaced8 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -10,7 +10,7 @@
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
 open CErrors
-open Term
+open Constr
 open Ccalgo
 open Pp
 
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index 9f53123db..a3e450134 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Ccalgo
-open Term
+open Constr
 
 type rule=
     Ax of constr
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 150319f6b..7dec34d4d 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -13,6 +13,7 @@ open Names
 open Inductiveops
 open Declarations
 open Term
+open Constr
 open EConstr
 open Vars
 open Tactics
@@ -76,11 +77,11 @@ let rec decompose_term env sigma t=
 	let (mind,i_ind),u = c in 
 	let u = EInstance.kind sigma u in
 	let canon_mind = MutInd.make1 (MutInd.canonical mind) in
-	let canon_ind = canon_mind,i_ind in  (Symb (Term.mkIndU (canon_ind,u)))
+	let canon_ind = canon_mind,i_ind in  (Symb (Constr.mkIndU (canon_ind,u)))
     | Const (c,u) -> 
 	let u = EInstance.kind sigma u in
 	let canon_const = Constant.make1 (Constant.canonical c) in 
-	  (Symb (Term.mkConstU (canon_const,u)))
+	  (Symb (Constr.mkConstU (canon_const,u)))
     | Proj (p, c) -> 
 	let canon_const kn = Constant.make1 (Constant.canonical kn) in 
 	let p' = Projection.map canon_const p in
@@ -198,7 +199,7 @@ let make_prb gls depth additionnal_terms =
       (fun decl ->
          let id = NamedDecl.get_id decl in
 	 begin
-	   let cid=Term.mkVar id in
+	   let cid=Constr.mkVar id in
 	   match litteral_of_constr env sigma (NamedDecl.get_type decl) with
 	       `Eq (t,a,b) -> add_equality state cid a b
 	     | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 6d3d4b743..fb65a8639 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -6,9 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Constr
 open Context.Named.Declaration
 
-let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
+let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Entries.const_entry_body)
     : Safe_typing.private_constants Entries.const_entry_body =
   Future.chain x begin fun ((b,ctx),fx) ->
     (f b , ctx) , fx
@@ -67,7 +68,7 @@ let start_deriving f suchthat lemma =
       let f_def = { f_def with Entries.const_entry_opaque = false } in
       let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in
       let f_kn = Declare.declare_constant f f_def in
-      let f_kn_term = Term.mkConst f_kn in
+      let f_kn_term = mkConst f_kn in
       (** In the type and body of the proof of [suchthat] there can be
           references to the variable [f]. It needs to be replaced by
           references to the constant [f] declared above. This substitution
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 3c46d5c43..bc84df76b 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Miniml
-open Term
+open Constr
 open Declarations
 open Names
 open ModPath
@@ -138,7 +138,7 @@ let check_arity env cb =
 let check_fix env cb i =
   match cb.const_body with
     | Def lbody ->
-	(match kind_of_term (Mod_subst.force_constr lbody) with
+	(match Constr.kind (Mod_subst.force_constr lbody) with
 	  | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
 	  | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd)
 	  | _ -> raise Impossible)
@@ -146,8 +146,8 @@ let check_fix env cb i =
 
 let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) =
   Array.equal Name.equal na1 na2 &&
-  Array.equal eq_constr ca1 ca2 &&
-  Array.equal eq_constr ta1 ta2
+  Array.equal Constr.equal ca1 ca2 &&
+  Array.equal Constr.equal ta1 ta2
 
 let factor_fix env l cb msb =
   let _,recd as check = check_fix env cb 0 in
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 7bbb825b1..dd8617738 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -34,4 +34,4 @@ val print_one_decl :
 (* Used by Extraction Compute *)
 
 val structure_for_compute :
-  Term.constr -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type
+  Constr.t -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a227478d0..47e812319 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -10,6 +10,7 @@
 open Util
 open Names
 open Term
+open Constr
 open Vars
 open Declarations
 open Declareops
@@ -81,7 +82,7 @@ let whd_betaiotazeta t =
 
 let rec flag_of_type env t : flag =
   let t = whd_all env t in
-  match kind_of_term t with
+  match Constr.kind t with
     | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c
     | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
     | Sort _ -> (Info,TypeScheme)
@@ -111,14 +112,14 @@ let push_rel_assum (n, t) env =
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
 let rec type_sign env c =
-  match kind_of_term (whd_all env c) with
+  match Constr.kind (whd_all env c) with
     | Prod (n,t,d) ->
 	(if is_info_scheme env t then Keep else Kill Kprop)
 	:: (type_sign (push_rel_assum (n,t) env) d)
     | _ -> []
 
 let rec type_scheme_nb_args env c =
-  match kind_of_term (whd_all env c) with
+  match Constr.kind (whd_all env c) with
     | Prod (n,t,d) ->
 	let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in
 	if is_info_scheme env t then n+1 else n
@@ -145,7 +146,7 @@ let make_typvar n vl =
   next_ident_away id' vl
 
 let rec type_sign_vl env c =
-  match kind_of_term (whd_all env c) with
+  match Constr.kind (whd_all env c) with
     | Prod (n,t,d) ->
 	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
 	if not (is_info_scheme env t) then Kill Kprop::s, vl
@@ -153,7 +154,7 @@ let rec type_sign_vl env c =
     | _ -> [],[]
 
 let rec nb_default_params env c =
-  match kind_of_term (whd_all env c) with
+  match Constr.kind (whd_all env c) with
     | Prod (n,t,d) ->
 	let n = nb_default_params (push_rel_assum (n,t) env) d in
 	if is_default env t then n+1 else n
@@ -207,7 +208,7 @@ let parse_ind_args si args relmax =
     | [] -> Int.Map.empty
     | Kill _ :: s -> parse (i+1) j s
     | Keep :: s ->
-      (match kind_of_term args.(i-1) with
+      (match Constr.kind args.(i-1) with
 	 | Rel k -> Int.Map.add (relmax+1-k) j (parse (i+1) (j+1) s)
 	 | _ -> parse (i+1) (j+1) s)
   in parse 1 1 si
@@ -224,7 +225,7 @@ let parse_ind_args si args relmax =
 
 
 let rec extract_type env db j c args =
-  match kind_of_term (whd_betaiotazeta c) with
+  match Constr.kind (whd_betaiotazeta c) with
     | App (d, args') ->
 	(* We just accumulate the arguments. *)
 	extract_type env db j d (Array.to_list args' @ args)
@@ -299,7 +300,7 @@ let rec extract_type env db j c args =
     | Proj (p,t) ->
        (* Let's try to reduce, if it hasn't already been done. *)
        if Projection.unfolded p then Tunknown
-       else extract_type env db j (Term.mkProj (Projection.unfold p, t)) args
+       else extract_type env db j (mkProj (Projection.unfold p, t)) args
     | Case _ | Fix _ | CoFix _ -> Tunknown
     | _ -> assert false
 
@@ -331,7 +332,7 @@ and extract_type_scheme env db c p =
   if Int.equal p 0 then extract_type env db 0 c []
   else
     let c = whd_betaiotazeta c in
-    match kind_of_term c with
+    match Constr.kind c with
       | Lambda (n,t,d) ->
           extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
       | _ ->
@@ -415,8 +416,8 @@ and extract_really_ind env kn mib =
 	  let t = snd (decompose_prod_n npar types.(j)) in
 	  let prods,head = dest_prod epar t in
 	  let nprods = List.length prods in
-          let args = match kind_of_term head with
-            | App (f,args) -> args (* [kind_of_term f = Ind ip] *)
+          let args = match Constr.kind head with
+            | App (f,args) -> args (* [Constr.kind f = Ind ip] *)
             | _ -> [||]
           in
 	  let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in
@@ -444,7 +445,7 @@ and extract_really_ind env kn mib =
 	if Option.is_empty mib.mind_record then raise (I Standard);
 	(* Now we're sure it's a record. *)
 	(* First, we find its field names. *)
-	let rec names_prod t = match kind_of_term t with
+	let rec names_prod t = match Constr.kind t with
 	  | Prod(n,_,t) -> n::(names_prod t)
 	  | LetIn(_,_,_,t) -> names_prod t
 	  | Cast(t,_,_) -> names_prod t
@@ -503,7 +504,7 @@ and extract_really_ind env kn mib =
 *)
 
 and extract_type_cons env db dbmap c i =
-  match kind_of_term (whd_all env c) with
+  match Constr.kind (whd_all env c) with
     | Prod (n,t,d) ->
 	let env' = push_rel_assum (n,t) env in
 	let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in
@@ -564,7 +565,7 @@ let record_constant_type env kn opt_typ =
 (* [mlt] is the ML type we want our extraction of [(c args)] to have. *)
 
 let rec extract_term env mle mlt c args =
-  match kind_of_term c with
+  match Constr.kind c with
     | App (f,a) ->
 	extract_term env mle mlt f (Array.to_list a @ args)
     | Lambda (n, t, d) ->
@@ -874,7 +875,7 @@ let decomp_lams_eta_n n m env c t =
 (* Let's try to identify some situation where extracted code
    will allow generalisation of type variables *)
 
-let rec gentypvar_ok c = match kind_of_term c with
+let rec gentypvar_ok c = match Constr.kind c with
   | Lambda _ | Const _ -> true
   | App (c,v) ->
       (* if all arguments are variables, these variables will
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index e1d43f340..b15b88ed2 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -9,7 +9,7 @@
 (*s Extraction from Coq terms to Miniml. *)
 
 open Names
-open Term
+open Constr
 open Declarations
 open Environ
 open Miniml
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index cc93f294b..e52e419fd 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -180,7 +180,7 @@ val implicits_of_global : global_reference -> Int.Set.t
 (*s Table for user-given custom ML extractions. *)
 
 (* UGLY HACK: registration of a function defined in [extraction.ml] *)
-val type_scheme_nb_args_hook : (Environ.env -> Term.constr -> int) Hook.t
+val type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t
 
 val is_custom : global_reference -> bool
 val is_inline_custom : global_reference -> bool
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index db1a46a03..c55040df0 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -8,7 +8,7 @@
 
 open Hipattern
 open Names
-open Term
+open Constr
 open EConstr
 open Vars
 open Termops
@@ -39,7 +39,7 @@ exception Is_atom of constr
 let meta_succ m = m+1
 
 let rec nb_prod_after n c=
-  match kind_of_term c with
+  match Constr.kind c with
     | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else
 	1+(nb_prod_after 0 b)
     | _ -> 0
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 106c469c6..3b6b711c0 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Constr
 open EConstr
 open Globnames
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index c2606dbe8..3409471a7 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -24,7 +24,7 @@ open Misctypes
 open Context.Rel.Declaration
 
 let compare_instance inst1 inst2=
-        let cmp c1 c2 = OrderedConstr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
+        let cmp c1 c2 = Constr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
 	match inst1,inst2 with
 	    Phantom(d1),Phantom(d2)->
 	      (cmp d1 d2)
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index d8d4c1a38..5c46f4cec 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
-open EConstr
 open Names
+open Constr
+open EConstr
 open Globnames
 
 type tactic = unit Proofview.tactic
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 05194164b..ea2d076ed 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -54,13 +54,7 @@ struct
 	(priority e1.pat) - (priority e2.pat)
 end
 
-module OrderedConstr=
-struct
-  type t=Term.constr
-  let compare=Term.compare
-end
-
-type h_item = global_reference * (int*Term.constr) option
+type h_item = global_reference * (int*Constr.t) option
 
 module Hitem=
 struct
@@ -70,13 +64,13 @@ struct
     if c = 0 then
       let cmp (i1, c1) (i2, c2) =
         let c = Int.compare i1 i2 in
-        if c = 0 then OrderedConstr.compare c1 c2 else c
+        if c = 0 then Constr.compare c1 c2 else c
       in
       Option.compare cmp co1 co2
     else c
 end
 
-module CM=Map.Make(OrderedConstr)
+module CM=Map.Make(Constr)
 
 module History=Set.Make(Hitem)
 
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index ca6079c8b..7f4a6dd86 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -10,11 +10,9 @@ open EConstr
 open Formula
 open Globnames
 
-module OrderedConstr: Set.OrderedType with type t=Term.constr
+module CM: CSig.MapS with type key=Constr.t
 
-module CM: CSig.MapS with type key=Term.constr
-
-type h_item = global_reference * (int*Term.constr) option
+type h_item = global_reference * (int*Constr.t) option
 
 module History: Set.S with type elt = h_item
 
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index d3e8aeee8..390aa8c85 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Constr
 open EConstr
 
 exception UFAIL of constr*constr
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 68af1b3b6..d9e9375c0 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -12,7 +12,7 @@
 des inéquations et équations sont entiers. En attendant la tactique Field.
 *)
 
-open Term
+open Constr
 open Tactics
 open Names
 open Globnames
@@ -27,11 +27,7 @@ qui donne le coefficient d'un terme du calcul des constructions,
 qui est zéro si le terme n'y est pas.
 *)
 
-module Constrhash = Hashtbl.Make
-  (struct type t = constr
-	  let equal = eq_constr
-	  let hash = hash_constr
-   end)
+module Constrhash = Hashtbl.Make(Constr)
 
 type flin = {fhom: rational Constrhash.t;
              fcste:rational};;
@@ -84,7 +80,7 @@ let string_of_R_constant kn =
     | _ -> "constant_not_of_R"
 
 let rec string_of_R_constr c =
- match kind_of_term c with
+ match Constr.kind c with
    Cast (c,_,_) -> string_of_R_constr c
   |Const (c,_) -> string_of_R_constant c
   | _ -> "not_of_constant"
@@ -92,7 +88,7 @@ let rec string_of_R_constr c =
 exception NoRational
 
 let rec rational_of_constr c =
-  match kind_of_term c with
+  match Constr.kind c with
   | Cast (c,_,_) -> (rational_of_constr c)
   | App (c,args) ->
       (match (string_of_R_constr c) with
@@ -125,7 +121,7 @@ exception NoLinear
 
 let rec flin_of_constr c =
   try(
-    match kind_of_term c with
+    match Constr.kind c with
   | Cast (c,_,_) -> (flin_of_constr c)
   | App (c,args) ->
       (match (string_of_R_constr c) with
@@ -192,9 +188,9 @@ exception NoIneq
 let ineq1_of_constr (h,t) =
   let h = EConstr.Unsafe.to_constr h in
   let t = EConstr.Unsafe.to_constr t in
-    match (kind_of_term t) with
+    match (Constr.kind t) with
       | App (f,args) ->
-        (match kind_of_term f with
+        (match Constr.kind f with
           | Const (c,_) when Array.length args = 2 ->
             let t1= args.(0) in
             let t2= args.(1) in
@@ -233,7 +229,7 @@ let ineq1_of_constr (h,t) =
             let t0= args.(0) in
             let t1= args.(1) in
             let t2= args.(2) in
-	    (match (kind_of_term t0) with
+	    (match (Constr.kind t0) with
               | Const (c,_) ->
 		(match (string_of_R_constant c) with
 		  | "R"->
@@ -438,7 +434,7 @@ let tac_use h =
 
 (*
 let is_ineq (h,t) =
-    match (kind_of_term t) with
+    match (Constr.kind t) with
 	App (f,args) ->
 	  (match (string_of_R_constr f) with
 	       "Rlt" -> true
@@ -479,7 +475,7 @@ let rec fourier () =
     (* si le but est une inéquation, on introduit son contraire,
        et le but à prouver devient False *)
     try 
-      match (kind_of_term goal) with
+      match (Constr.kind goal) with
       App (f,args) ->
       let get = eget in
       (match (string_of_R_constr f) with
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 018b51517..722dbc16b 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -2,6 +2,7 @@ open Printer
 open CErrors
 open Util
 open Term
+open Constr
 open Vars
 open Namegen
 open Names
@@ -80,7 +81,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let is_pte =
     let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in
     fun t ->
-      match kind_of_term t with
+      match Constr.kind t with
 	| Var id -> Id.Set.mem id set
 	| _ -> false
   in
@@ -100,13 +101,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let pre_princ = EConstr.Unsafe.to_constr pre_princ in
   let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
   let is_dom c =
-    match kind_of_term c with
+    match Constr.kind c with
       | Ind((u,_),_) -> MutInd.equal u rel_as_kn
       | Construct(((u,_),_),_) -> MutInd.equal u rel_as_kn
       | _ -> false
   in
   let get_fun_num c =
-    match kind_of_term c with
+    match Constr.kind c with
       | Ind((_,num),_) -> num
       | Construct(((_,num),_),_) -> num
       | _ -> assert false
@@ -119,7 +120,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   in
   let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
     let (new_princ_type,_) as res =
-      match kind_of_term pre_princ with
+      match Constr.kind pre_princ with
 	| Rel n ->
 	    begin
 	      try match Environ.lookup_rel n env with
@@ -149,12 +150,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	    in
 	    let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in
 	    applistc new_f new_args,
-	    list_union_eq eq_constr binders_to_remove_from_f binders_to_remove
+	    list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove
 	| LetIn(x,v,t,b) ->
 	    compute_new_princ_type_for_letin remove env x v t b
 	| _ -> pre_princ,[]
     in
-(*     let _ = match kind_of_term pre_princ with *)
+(*     let _ = match Constr.kind pre_princ with *)
 (* 	| Prod _ -> *)
 (* 	    observe(str "compute_new_princ_type for "++ *)
 (* 	      pr_lconstr_env env pre_princ ++ *)
@@ -170,13 +171,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	let new_x : Name.t = get_name (Termops.ids_of_context env) x in
 	let new_env = Environ.push_rel (LocalAssum (x,t)) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
-	 if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	 then (pop new_b), filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+	 if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
+	 then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
 	 else
 	   (
 	     bind_fun(new_x,new_t,new_b),
 	     list_union_eq
-	       eq_constr
+	       Constr.equal
 	       binders_to_remove_from_t
 	       (List.map pop binders_to_remove_from_b)
 	   )
@@ -189,7 +190,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	| Toberemoved_with_rel (n,c) ->
 (* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+	    new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b)
     end
   and compute_new_princ_type_for_letin remove env x v t b =
     begin
@@ -199,14 +200,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	let new_x : Name.t = get_name (Termops.ids_of_context env) x in
 	let new_env = Environ.push_rel (LocalDef (x,v,t)) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
-	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+	if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
+	then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
 	else
 	  (
 	    mkLetIn(new_x,new_v,new_t,new_b),
 	    list_union_eq
-	      eq_constr
-	      (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
+	      Constr.equal
+	      (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v)
 	      (List.map pop binders_to_remove_from_b)
 	  )
 
@@ -218,12 +219,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	| Toberemoved_with_rel (n,c) ->
 (* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+	    new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b)
     end
   and  compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc)  =
     let new_e,to_remove_from_e = compute_new_princ_type remove env e
     in
-    new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
+    new_e::c_acc,list_union_eq Constr.equal to_remove_from_e to_remove_acc
   in
 (*   observe (str "Computing new principe from " ++ pr_lconstr_env  env_with_params_and_predicates pre_princ); *)
   let pre_res,_ =
@@ -329,7 +330,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
       | Some (id) -> id,id
       | None ->
 	  let id_of_f = Label.to_id (Constant.label (fst f)) in
-	  id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
+	  id_of_f,Indrec.make_elimination_ident id_of_f (Sorts.family type_sort)
   in
   let names = ref [new_princ_name] in
   let hook =
@@ -389,7 +390,7 @@ exception Not_Rec
 
 let get_funs_constant mp dp =
   let get_funs_constant const e : (Names.Constant.t*int) array =
-    match kind_of_term ((strip_lam e)) with
+    match Constr.kind ((strip_lam e)) with
       | Fix((_,(na,_,_))) ->
 	  Array.mapi
 	    (fun i na ->
@@ -430,7 +431,7 @@ let get_funs_constant mp dp =
       let first_params = List.hd l_params  in
       List.iter
 	(fun params ->
-	   if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && eq_constr c1 c2) first_params params)
+	   if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && Constr.equal c1 c2) first_params params)
 	   then user_err Pp.(str "Not a mutal recursive block")
 	)
 	l_params
@@ -439,7 +440,7 @@ let get_funs_constant mp dp =
     let _check_bodies =
       try
 	let extract_info is_first body =
-	  match kind_of_term body with
+	  match Constr.kind body with
 	    | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
 	    | _ ->
 		if is_first && Int.equal (List.length l_bodies) 1
@@ -450,7 +451,7 @@ let get_funs_constant mp dp =
 	let check body  = (* Hope this is correct *)
 	  let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) =
             Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 &&
-            Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2
+            Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2
 	  in
 	  if not (eq_infos first_infos (extract_info false body))
 	  then  user_err Pp.(str "Not a mutal recursive block")
@@ -574,7 +575,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
 		let t =  (strip_prod_assum t) in
 		let applied_g = List.hd (List.rev (snd (decompose_app t))) in
 		let g = fst (decompose_app applied_g) in
-		if eq_constr f g
+		if Constr.equal f g
 		then raise (Found_type j);
 		observe (Printer.pr_lconstr f ++ str " <> " ++
 			   Printer.pr_lconstr g)
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 2eb1b7935..a3315f22c 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 
 val generate_functional_principle :
   Evd.evar_map ref -> 
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index e8e5bfccc..8ab6dbcdf 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -2,6 +2,7 @@ open Printer
 open Pp
 open Names
 open Term
+open Constr
 open Vars
 open Glob_term
 open Glob_ops
@@ -1015,7 +1016,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
 		    observe (str " computing new type for jmeq : done") ;
 		    let new_args =
-		      match kind_of_term eq'_as_constr with
+		      match Constr.kind eq'_as_constr with
 			| App(_,[|_;_;ty;_|]) ->
 			    let ty = Array.to_list (snd (destApp ty)) in
 			    let ty' = snd (Util.List.chop nparam ty) in
@@ -1297,7 +1298,7 @@ let rec rebuild_return_type rt =
 			    CAst.make @@ Constrexpr.CSort(GType []))
 
 let do_build_inductive
-      evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
+      evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
       returned_types
       (rtl:glob_constr list) =
   let _time1 = System.get_time () in
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 0cab5a6d3..ff0e98d00 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -11,7 +11,7 @@ val build_inductive :
   Id.t list -> (* The list of function name *) 
  *)
   Evd.evar_map ->
-  Term.pconstant list -> 
+  Constr.pconstant list -> 
   (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list list -> (* The list of function args *)
   Constrexpr.constr_expr list -> (* The list of function returned type *)
   Glob_term.glob_constr list -> (* the list of body *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 76fcd5ec8..e9102e9c8 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,8 +1,10 @@
 open Names
 open Pp
+open Constr
 open Libnames
 open Globnames
 open Refiner
+
 let mk_prefix pre id = Id.of_string (pre^(Id.to_string id))
 let mk_rel_id = mk_prefix "R_"
 let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
@@ -111,7 +113,7 @@ let const_of_id id =
       (str "cannot find " ++ Id.print id)
 
 let def_of_const t =
-   match (Term.kind_of_term t) with
+   match Constr.kind t with
     Term.Const sp ->
       (try (match Environ.constant_opt_value_in (Global.env()) sp with
              | Some c -> c
@@ -330,8 +332,6 @@ let discharge_Function (_,finfos) =
 	   is_general = finfos.is_general
 	 }
 
-open Term
-
 let pr_ocst c =
   Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ())
 
@@ -545,9 +545,9 @@ let prodn n env b =
 (* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *)
 let compose_prod l b = prodn (List.length l) l b
 
-type tcc_lemma_value = 
+type tcc_lemma_value =
   | Undefined
-  | Value of Term.constr
+  | Value of constr
   | Not_needed
 
 (* We only "purify" on exceptions *)
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index d41abee87..5cc7163aa 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -38,7 +38,7 @@ val chop_rlambda_n : int -> Glob_term.glob_constr ->
 val chop_rprod_n : int -> Glob_term.glob_constr ->
   (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr
 
-val def_of_const : Term.constr -> Term.constr
+val def_of_const : Constr.t -> Constr.t
 val eq : EConstr.constr Lazy.t
 val refl_equal : EConstr.constr Lazy.t
 val const_of_id: Id.t ->  Globnames.global_reference(* constantyes *)
@@ -118,10 +118,10 @@ val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
   (Names.Name.t * EConstr.t) list * EConstr.t
 val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
 val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
-                                                        
-type tcc_lemma_value = 
+
+type tcc_lemma_value =
   | Undefined
-  | Value of Term.constr
+  | Value of Constr.t
   | Not_needed
 
 val funind_purify : ('a -> 'b) -> ('a -> 'b)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 93317fce1..692a874d3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -12,6 +12,7 @@ open CErrors
 open Util
 open Names
 open Term
+open Constr
 open EConstr
 open Vars
 open Pp
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 77c26f8ce..b372241d2 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -18,6 +18,7 @@ open Vernacexpr
 open Pp
 open Names
 open Term
+open Constr
 open Vars
 open Declarations
 open Glob_term
@@ -36,19 +37,19 @@ let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
 
 (** Substitutions in constr *)
 let compare_constr_nosub t1 t2 =
-  if compare_constr (fun _ _ -> false) t1 t2
+  if Constr.compare_head (fun _ _ -> false) t1 t2
   then true
   else false
 
 let rec compare_constr' t1 t2 =
   if compare_constr_nosub t1 t2
   then true
-  else (compare_constr (compare_constr') t1 t2)
+  else (Constr.compare_head (compare_constr') t1 t2)
 
 let rec substitterm prof t by_t in_u =
   if (compare_constr' (lift prof t) in_u)
   then (lift prof by_t)
-  else map_constr_with_binders succ
+  else Constr.map_with_binders succ
     (fun i -> substitterm i t by_t) prof in_u
 
 let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl
@@ -954,16 +955,16 @@ let funify_branches relinfo nfuns branch =
       | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind
       | _ -> assert false in
   let is_dom c =
-    match kind_of_term c with
+    match Constr.kind c with
       | Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct
       | _ -> false in
   let _dom_i c =
     assert (is_dom c);
-    match kind_of_term c with
+    match Constr.kind c with
       | Ind((u,i)) | Construct((u,_),i) -> i
       | _ -> assert false in
   let _is_pred c shift =
-    match kind_of_term c with
+    match Constr.kind c with
       | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches)
       | _ -> false in
   (* FIXME: *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 76f859ed7..2fdc3bc37 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -10,6 +10,7 @@
 module CVars = Vars
 
 open Term
+open Constr
 open EConstr
 open Vars
 open Namegen
@@ -69,7 +70,7 @@ let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value =
 let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None)))
 
 let def_of_const t =
-   match (kind_of_term t) with
+   match (Constr.kind t) with
     Const sp ->
       (try (match constant_opt_value_in (Global.env ()) sp with
              | Some c -> c
@@ -143,7 +144,7 @@ let nat = function () -> (coq_init_constant "nat")
 let iter_ref () =  
   try find_reference ["Recdef"] "iter" 
   with Not_found -> user_err Pp.(str "module Recdef not loaded")
-let iter = function () -> (constr_of_global (delayed_force iter_ref))
+let iter_rd = function () -> (constr_of_global (delayed_force iter_ref))
 let eq = function () -> (coq_init_constant "eq")
 let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
 let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm")
@@ -175,8 +176,9 @@ let simpl_iter clause =
     clause
 
 (* Others ugly things ... *)
-let (value_f:Term.constr list -> global_reference -> Term.constr) =
+let (value_f: Constr.t list -> global_reference -> Constr.t) =
   let open Term in
+  let open Constr in
   fun al fterm ->
     let rev_x_id_l =
       (
@@ -207,7 +209,7 @@ let (value_f:Term.constr list -> global_reference -> Term.constr) =
     let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
     it_mkLambda_or_LetIn body context
 
-let (declare_f : Id.t -> logical_kind -> Term.constr list -> global_reference -> global_reference) =
+let (declare_f : Id.t -> logical_kind -> Constr.t list -> global_reference -> global_reference) =
   fun f_id kind input_type fterm_ref ->
     declare_fun f_id kind (value_f input_type fterm_ref);;
 
@@ -1039,11 +1041,12 @@ let prove_eq = travel equation_info
 *)
 let compute_terminate_type nb_args func =
   let open Term in
+  let open Constr in
   let open CVars in
   let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in
   let rev_args,b = decompose_prod_n nb_args a_arrow_b in
   let left =
-    mkApp(delayed_force iter,
+    mkApp(delayed_force iter_rd,
 	  Array.of_list
 	    (lift 5 a_arrow_b:: mkRel 3::
 	       constr_of_global func::mkRel 1::
@@ -1460,7 +1463,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
 
 let (com_eqn : int -> Id.t ->
        global_reference -> global_reference -> global_reference
-	 -> Term.constr -> unit) =
+	 -> Constr.t -> unit) =
   fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
     let open CVars in
     let opacity =
@@ -1514,6 +1517,7 @@ let (com_eqn : int -> Id.t ->
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
     generate_induction_principle using_lemmas : unit =
   let open Term in
+  let open Constr in
   let open CVars in
   let env = Global.env() in
   let evd = ref (Evd.from_env env) in
@@ -1536,7 +1540,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 (*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
 (*     Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)
 (*     Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *)
-    match kind_of_term eq' with
+    match Constr.kind eq' with
       | App(e,[|_;_;eq_fix|]) ->
 	  mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars  eq_fix))
       | _ -> failwith "Recursive Definition (res not eq)"
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 63bbdbe7e..50b84731b 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,3 +1,4 @@
+open Constr
 
 (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
 val tclUSER_if_not_mes : 
@@ -11,9 +12,9 @@ bool ->
            Constrintern.internalization_env ->
            Constrexpr.constr_expr ->
            Constrexpr.constr_expr ->
-           int -> Constrexpr.constr_expr -> (Term.pconstant ->
+           int -> Constrexpr.constr_expr -> (pconstant ->
             Indfun_common.tcc_lemma_value ref ->
-            Term.pconstant ->
-            Term.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit
+            pconstant ->
+            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit
 
 
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 65c186a41..4b1555e55 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -415,7 +415,7 @@ VERNAC COMMAND EXTEND DeriveInversionClear
   -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
 
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ]
-  -> [ add_inversion_lemma_exn na c InProp false inv_clear_tac ]
+  -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_clear_tac ]
 END
 
 VERNAC COMMAND EXTEND DeriveInversion
@@ -424,7 +424,7 @@ VERNAC COMMAND EXTEND DeriveInversion
   -> [ add_inversion_lemma_exn na c s false inv_tac ]
 
 | [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ]
-  -> [ add_inversion_lemma_exn na c InProp false inv_tac ]
+  -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_tac ]
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversion
@@ -514,7 +514,7 @@ let cache_transitivity_lemma (_,(left,lem)) =
 
 let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)
 
-let inTransitivity : bool * Term.constr -> obj =
+let inTransitivity : bool * Constr.t -> obj =
   declare_object {(default_object "TRANSITIVITY-STEPS") with
     cache_function = cache_transitivity_lemma;
     open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o);
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 104977aef..ed2d9da63 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -91,7 +91,7 @@ END
 
 (** TODO: DEPRECATE *)
 (* A progress test that allows to see if the evars have changed *)
-open Term
+open Constr
 open Proofview.Notations
 
 let rec eq_constr_mod_evars sigma x y =
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index e467d3e2c..6522fc28f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1120,10 +1120,10 @@ let pr_goal_selector ~toplevel s =
     let ty = EConstr.Unsafe.to_constr ty in
     let rec strip_ty acc n ty =
       if n=0 then (List.rev acc, EConstr.of_constr ty) else
-        match Term.kind_of_term ty with
-            Term.Prod(na,a,b) ->
-              strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
-          | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
+        match Constr.kind ty with
+        | Constr.Prod(na,a,b) ->
+          strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
+        | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
   let pr_atomic_tactic_level env sigma n t =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1809f0fcd..705a51edd 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -12,7 +12,7 @@ open CErrors
 open Util
 open Nameops
 open Namegen
-open Term
+open Constr
 open EConstr
 open Vars
 open Reduction
@@ -426,7 +426,7 @@ let split_head = function
   | [] -> assert(false)
 
 let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') =
-  pb == pb' || (ty == ty' && Term.eq_constr x x' && Term.eq_constr y y')
+  pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y')
 
 let problem_inclusion x y =
   List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x
@@ -928,8 +928,8 @@ let fold_match ?(force=false) env sigma c =
 	it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx)
     in
     let sk = 
-      if sortp == InProp then
-	if sortc == InProp then
+      if sortp == Sorts.InProp then
+	if sortc == Sorts.InProp then
 	  if dep then case_dep_scheme_kind_from_prop
 	  else case_scheme_kind_from_prop
 	else (
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 63e891b45..1306c590b 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -37,7 +37,7 @@ type ('constr,'redexpr) strategy_ast =
 
 type rewrite_proof = 
   | RewPrf of constr * constr
-  | RewCast of Term.cast_kind
+  | RewCast of Constr.cast_kind
 
 type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 4d171ecbc..c03a86732 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -8,7 +8,7 @@
 
 open Util
 open Names
-open Term
+open Constr
 open EConstr
 open Misctypes
 open Genarg
@@ -172,8 +172,8 @@ let id_of_name = function
        | Sort s ->
 	  begin
 	    match ESorts.kind sigma s with
-	    | Prop _ -> Label.to_id (Label.make "Prop")
-	    | Type _ -> Label.to_id (Label.make "Type")
+	    | Sorts.Prop _ -> Label.to_id (Label.make "Prop")
+	    | Sorts.Type _ -> Label.to_id (Label.make "Type")
 	  end
        | _ -> fail()
 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index fc6781b06..218342efe 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -20,6 +20,7 @@ open Pp
 open Mutils
 open Goptions
 open Names
+open Constr
 
 (**
   * Debug flag 
@@ -580,9 +581,9 @@ struct
     | Ukn
     | BadStr of string
     | BadNum of int
-    | BadTerm of Term.constr
+    | BadTerm of constr
     | Msg   of string
-    | Goal of (Term.constr list ) * Term.constr * parse_error
+    | Goal of (constr list ) * constr * parse_error
 
   let string_of_error = function
    | Ukn -> "ukn"
@@ -1521,7 +1522,7 @@ let rec witness prover   l1 l2 =
 let rec apply_ids t ids =
  match ids with
   | [] -> t
-  | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids
+  | i::ids -> apply_ids (mkApp(t,[| mkVar i |])) ids
 
 let coq_Node = 
  lazy (gen_constant_in_modules "VarMap"
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 72934a15d..559dfab52 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -8,7 +8,7 @@
 
 open CErrors
 open Util
-open Term
+open Constr
 open Tactics
 open Coqlib
 
@@ -204,42 +204,42 @@ else
     mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (num_of_int n)]
 
 let rec parse_pos p =
-  match kind_of_term p with
+  match Constr.kind p with
 | App (a,[|p2|]) ->
-    if eq_constr a (Lazy.force pxO) then num_2 */ (parse_pos p2)
+    if Constr.equal a (Lazy.force pxO) then num_2 */ (parse_pos p2)
     else num_1 +/ (num_2 */ (parse_pos p2))
 | _ -> num_1
 
 let parse_z z =
-  match kind_of_term z with
+  match Constr.kind z with
 | App (a,[|p2|]) ->
-    if eq_constr a (Lazy.force zpos) then parse_pos p2 else (num_0 -/ (parse_pos p2))
+    if Constr.equal a (Lazy.force zpos) then parse_pos p2 else (num_0 -/ (parse_pos p2))
 | _ -> num_0
 
 let parse_n z =
-  match kind_of_term z with
+  match Constr.kind z with
 | App (a,[|p2|]) ->
     parse_pos p2
 | _ -> num_0
 
 let rec parse_term p =
-  match kind_of_term p with
+  match Constr.kind p with
 | App (a,[|_;p2|]) ->
-    if eq_constr a (Lazy.force ttvar) then Var (string_of_num (parse_pos p2))
-    else if eq_constr a (Lazy.force ttconst) then Const (parse_z p2)
-    else if eq_constr a (Lazy.force ttopp) then Opp (parse_term p2)
+    if Constr.equal a (Lazy.force ttvar) then Var (string_of_num (parse_pos p2))
+    else if Constr.equal a (Lazy.force ttconst) then Const (parse_z p2)
+    else if Constr.equal a (Lazy.force ttopp) then Opp (parse_term p2)
     else Zero
 | App (a,[|_;p2;p3|]) ->
-    if eq_constr a (Lazy.force ttadd) then Add (parse_term p2, parse_term p3)
-    else if eq_constr a (Lazy.force ttsub) then Sub (parse_term p2, parse_term p3)
-    else if eq_constr a (Lazy.force ttmul) then Mul (parse_term p2, parse_term p3)
-    else if eq_constr a (Lazy.force ttpow) then
+    if Constr.equal a (Lazy.force ttadd) then Add (parse_term p2, parse_term p3)
+    else if Constr.equal a (Lazy.force ttsub) then Sub (parse_term p2, parse_term p3)
+    else if Constr.equal a (Lazy.force ttmul) then Mul (parse_term p2, parse_term p3)
+    else if Constr.equal a (Lazy.force ttpow) then
       Pow (parse_term p2, int_of_num (parse_n p3))
     else Zero
 | _ -> Zero
 
 let rec parse_request lp =
-  match kind_of_term lp with
+  match Constr.kind lp with
     | App (_,[|_|])  -> []
     | App (_,[|_;p;lp1|])  ->
 	(parse_term p)::(parse_request lp1)
diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli
index d6e3071aa..e50a12a50 100644
--- a/plugins/nsatz/nsatz.mli
+++ b/plugins/nsatz/nsatz.mli
@@ -6,4 +6,4 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-val nsatz_compute : Term.constr -> unit Proofview.tactic
+val nsatz_compute : Constr.t -> unit Proofview.tactic
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index e1e73b1c3..96bf31b11 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -166,11 +166,7 @@ exchange ?1 and ?2 in the example above)
 
 *)
 
-module ConstrSet = Set.Make(
-  struct
-    type t = Term.constr
-    let compare = Term.compare
-  end)
+module ConstrSet = Set.Make(Constr)
 
 type inversion_scheme = {
   normal_lhs_rhs : (constr * constr_pattern) list;
@@ -385,11 +381,7 @@ let rec sort_subterm gl l =
     | [] -> []
     | h::t -> insert h (sort_subterm gl t)
 
-module Constrhash = Hashtbl.Make
-  (struct type t = Term.constr
-	  let equal = Term.eq_constr
-	  let hash = Term.hash_constr
-   end)
+module Constrhash = Hashtbl.Make(Constr)
 
 let subst_meta subst c =
   let subst = List.map (fun (i, c) -> i, EConstr.Unsafe.to_constr c) subst in
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
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 9f02388c3..150c253a7 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -13,6 +13,7 @@ open Ltac_plugin
 open CErrors
 open Util
 open Term
+open Constr
 open Tacmach
 open Proof_search
 open Context.Named.Declaration
@@ -82,7 +83,7 @@ let make_atom atom_env term=
   let term = EConstr.Unsafe.to_constr term in
   try
     let (_,i)=
-      List.find (fun (t,_)-> eq_constr term t) atom_env.env
+      List.find (fun (t,_)-> Constr.equal term t) atom_env.env
     in Atom i
   with Not_found ->
     let i=atom_env.next in
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index bec18f6df..b2285a4a1 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -10,7 +10,7 @@
 
 type atom_env=
     {mutable next:int;
-     mutable env:(Term.constr*int) list}
+     mutable env:(Constr.t*int) list}
 
 val make_form : atom_env ->
     Goal.goal Evd.sigma -> EConstr.types -> Proof_search.form
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b8fae2494..9e4b896f8 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -10,7 +10,7 @@ open Ltac_plugin
 open Pp
 open Util
 open Names
-open Term
+open Constr
 open EConstr
 open Vars
 open CClosure
@@ -58,13 +58,13 @@ let rec mk_clos_but f_map subs t =
   match f_map (global_of_constr_nofail t) with
     | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t
     | None ->
-        (match kind_of_term t with
+        (match Constr.kind t with
             App(f,args) -> mk_clos_app_but f_map subs f args 0
           | Prod _ -> mk_clos_deep (mk_clos_but f_map) subs t
           | _ -> mk_atom t)
 
 and mk_clos_app_but f_map subs f args n =
-  let open Term in
+  let open Constr in
   if n >= Array.length args then mk_atom(mkApp(f, args))
   else
     let fargs, args' = Array.chop n args in
@@ -151,7 +151,7 @@ let ic_unsafe c = (*FIXME remove *)
     EConstr.of_constr (fst (Constrintern.interp_constr env sigma c))
 
 let decl_constant na ctx c =
-  let open Term in
+  let open Constr in
   let vars = Univops.universes_of_constr c in
   let ctx = Univops.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
   mkConst(declare_constant (Id.of_string na) 
@@ -346,11 +346,7 @@ let _ = add_map "ring"
 
 let pr_constr c = pr_econstr c
 
-module M = struct
-  type t = Term.constr
-  let compare = Term.compare
-end
-module Cmap = Map.Make(M)
+module Cmap = Map.Make(Constr)
 
 let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
 let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table"
@@ -395,7 +391,7 @@ let subst_th (subst,th) =
   let posttac'= Tacsubst.subst_tactic subst th.ring_post_tac in
   if c' == th.ring_carrier &&
      eq' == th.ring_req &&
-     Term.eq_constr set' th.ring_setoid &&
+     Constr.equal set' th.ring_setoid &&
      ext' == th.ring_ext &&
      morph' == th.ring_morph &&
      th' == th.ring_th &&
@@ -933,7 +929,7 @@ let field_equality evd r inv req =
 	  inv_m_lem
 
 let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
-  let open Term in
+  let open Constr in
   check_required_library (cdir@["Field_tac"]);
   let (sigma,fth) = ic fth in
   let env = Global.env() in
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli
index d37582bd7..c26fcc8d1 100644
--- a/plugins/setoid_ring/newring_ast.mli
+++ b/plugins/setoid_ring/newring_ast.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Constr
 open Libnames
 open Constrexpr
 open Tacexpr
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1f2d02093..c1d7e6278 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Evd
 open Term
+open Constr
 open Termops
 open Printer
 open Locusops
@@ -465,7 +466,6 @@ let ssrevaltac ist gtac =
 (* but stripping global ones. We use the variable names to encode the    *)
 (* the number of dependencies, so that the transformation is reversible. *)
 
-open Term
 let env_size env = List.length (Environ.named_context env)
 
 let pf_concl gl = EConstr.Unsafe.to_constr (pf_concl gl)
@@ -491,23 +491,23 @@ let pf_abs_evars2 gl rigid (sigma, c0) =
     | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in
     let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in
     nf_evar sigma t in
-  let rec put evlist c = match kind_of_term c with
+  let rec put evlist c = match Constr.kind c with
   | Evar (k, a) ->  
     if List.mem_assoc k evlist || Evd.mem sigma0 k || List.mem k rigid then evlist else
     let n = max 0 (Array.length a - nenv) in
     let t = abs_evar n k in (k, (n, t)) :: put evlist t
-  | _ -> fold_constr put evlist c in
+  | _ -> Constr.fold put evlist c in
   let evlist = put [] c0 in
   if evlist = [] then 0, EConstr.of_constr c0,[], ucst else
   let rec lookup k i = function
     | [] -> 0, 0
     | (k', (n, _)) :: evl -> if k = k' then i, n else lookup k (i + 1) evl in
-  let rec get i c = match kind_of_term c with
+  let rec get i c = match Constr.kind c with
   | Evar (ev, a) ->
     let j, n = lookup ev i evlist in
-    if j = 0 then map_constr (get i) c else if n = 0 then mkRel j else
+    if j = 0 then Constr.map (get i) c else if n = 0 then mkRel j else
     mkApp (mkRel j, Array.init n (fun k -> get i a.(n - 1 - k)))
-  | _ -> map_constr_with_binders ((+) 1) get i c in
+  | _ -> Constr.map_with_binders ((+) 1) get i c in
   let rec loop c i = function
   | (_, (n, t)) :: evl ->
     loop (mkLambda (mk_evar_name n, get (i - 1) t, c)) (i - 1) evl
@@ -551,7 +551,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
     | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in
     let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in
     nf_evar sigma0 (nf_evar sigma t) in
-  let rec put evlist c = match kind_of_term c with
+  let rec put evlist c = match Constr.kind c with
   | Evar (k, a) ->  
     if List.mem_assoc k evlist || Evd.mem sigma0 k then evlist else
     let n = max 0 (Array.length a - nenv) in
@@ -560,7 +560,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
         (pf_env gl) sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k))) in
     let is_prop = k_ty = InProp in
     let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t
-  | _ -> fold_constr put evlist c in
+  | _ -> Constr.fold put evlist c in
   let evlist = put [] c0 in
   if evlist = [] then 0, c0 else
   let pr_constr t = Printer.pr_econstr (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in
@@ -588,17 +588,17 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   let rec lookup k i = function
     | [] -> 0, 0
     | (k', (n,_,_)) :: evl -> if k = k' then i,n else lookup k (i + 1) evl in
-  let rec get evlist i c = match kind_of_term c with
+  let rec get evlist i c = match Constr.kind c with
   | Evar (ev, a) ->
     let j, n = lookup ev i evlist in
-    if j = 0 then map_constr (get evlist i) c else if n = 0 then mkRel j else
+    if j = 0 then Constr.map (get evlist i) c else if n = 0 then mkRel j else
     mkApp (mkRel j, Array.init n (fun k -> get evlist i a.(n - 1 - k)))
-  | _ -> map_constr_with_binders ((+) 1) (get evlist) i c in
+  | _ -> Constr.map_with_binders ((+) 1) (get evlist) i c in
   let rec app extra_args i c = match decompose_app c with
   | hd, args when isRel hd && destRel hd = i ->
       let j = destRel hd in
       mkApp (mkRel j, Array.of_list (List.map (Vars.lift (i-1)) extra_args @ args))
-  | _ -> map_constr_with_binders ((+) 1) (app extra_args) i c in
+  | _ -> Constr.map_with_binders ((+) 1) (app extra_args) i c in
   let rec loopP evlist c i = function
   | (_, (n, t, _)) :: evl ->
     let t = get evlist (i - 1) t in
@@ -645,7 +645,7 @@ let pf_abs_cterm gl n c0 =
   let c0 = EConstr.Unsafe.to_constr c0 in
   let noargs = [|0|] in
   let eva = Array.make n noargs in
-  let rec strip i c = match kind_of_term c with
+  let rec strip i c = match Constr.kind c with
   | App (f, a) when isRel f ->
     let j = i - destRel f in
     if j >= n || eva.(j) = noargs then mkApp (f, Array.map (strip i) a) else
@@ -653,8 +653,8 @@ let pf_abs_cterm gl n c0 =
     let nd = Array.length dp - 1 in
     let mkarg k = strip i a.(if k < nd then dp.(k + 1) - j else k + dp.(0)) in
     mkApp (f, Array.init (Array.length a - dp.(0)) mkarg)
-  | _ -> map_constr_with_binders ((+) 1) strip i c in
-  let rec strip_ndeps j i c = match kind_of_term c with
+  | _ -> Constr.map_with_binders ((+) 1) strip i c in
+  let rec strip_ndeps j i c = match Constr.kind c with
   | Prod (x, t, c1) when i < j ->
     let dl, c2 = strip_ndeps j (i + 1) c1 in
     if Vars.noccurn 1 c2 then dl, Vars.lift (-1) c2 else
@@ -665,7 +665,7 @@ let pf_abs_cterm gl n c0 =
     if Vars.noccurn 1 c2 then dl, Vars.lift (-1) c2 else
     i :: dl, mkLetIn (x, strip i b, strip i t, c2)
   | _ -> [], strip i c in
-  let rec strip_evars i c = match kind_of_term c with
+  let rec strip_evars i c = match Constr.kind c with
     | Lambda (x, t1, c1) when i < n ->
       let na = nb_evar_deps x in
       let dl, t2 = strip_ndeps (i + na) i t1 in
@@ -760,7 +760,7 @@ let clear_with_wilds wilds clr0 gl =
     let id = NamedDecl.get_id nd in
     if List.mem id clr || not (List.mem id wilds) then clr else
     let vars = Termops.global_vars_set_of_decl (pf_env gl) (project gl) nd in
-    let occurs id' = Idset.mem id' vars in
+    let occurs id' = Id.Set.mem id' vars in
     if List.exists occurs clr then id :: clr else clr in
   Proofview.V82.of_tactic (Tactics.clear (Context.Named.fold_inside extend_clr ~init:clr0 (Tacmach.pf_hyps gl))) gl
 
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 2eadd5f26..c39945194 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -190,7 +190,7 @@ val pf_merge_uc_of :
 val constr_name : evar_map -> EConstr.t -> Name.t
 val pf_type_of :
            Goal.goal Evd.sigma ->
-           Term.constr -> Goal.goal Evd.sigma * Term.types
+           Constr.constr -> Goal.goal Evd.sigma * Constr.types
 val pfe_type_of :
            Goal.goal Evd.sigma ->
            EConstr.t -> Goal.goal Evd.sigma * EConstr.types
@@ -220,7 +220,7 @@ val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx
 val pf_fresh_global :
            Globnames.global_reference ->
            Goal.goal Evd.sigma ->
-           Term.constr * Goal.goal Evd.sigma
+           Constr.constr * Goal.goal Evd.sigma
 
 val is_discharged_id : Id.t -> bool
 val mk_discharged_id : Id.t -> Id.t
@@ -232,7 +232,7 @@ val new_tmp_id :
 val mk_anon_id : string -> Goal.goal Evd.sigma -> Id.t
 val pf_abs_evars_pirrel :
            Goal.goal Evd.sigma ->
-           evar_map * Term.constr -> int * Term.constr
+           evar_map * Constr.constr -> int * Constr.constr
 val pf_nbargs : Goal.goal Evd.sigma -> EConstr.t -> int
 val gen_tmp_ids : 
            ?ist:Geninterp.interp_sign ->
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 95ca6f49a..e82f222b9 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -11,13 +11,14 @@
 open Ltac_plugin
 open Util
 open Names
+open Term
+open Constr
 open Vars
 open Locus
 open Printer
 open Globnames
 open Termops
 open Tacinterp
-open Term
 
 open Ssrmatching_plugin
 open Ssrmatching
@@ -316,7 +317,7 @@ let rw_progress rhs lhs ise = not (EConstr.eq_constr ise lhs (Evarutil.nf_evar i
 (* such a generic Leibnitz equation -- short of inspecting the type  *)
 (* of the elimination lemmas.                                        *)
 
-let rec strip_prod_assum c = match Term.kind_of_term c with
+let rec strip_prod_assum c = match Constr.kind c with
   | Prod (_, _, c') -> strip_prod_assum c'
   | LetIn (_, v, _, c') -> strip_prod_assum (subst1 v c)
   | Cast (c', _, _) -> strip_prod_assum c'
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index d01bdc1b9..29e96ec59 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -32,6 +32,7 @@ let ssrposetac ist (id, (_, t)) gl =
 
 open Pp
 open Term
+open Constr
 
 let ssrsettac ist id ((_, (pat, pty)), (_, occ)) gl =
   let pat = interp_cpattern ist gl pat (Option.map snd pty) in
@@ -59,10 +60,10 @@ let rec is_Evar_or_CastedMeta sigma x =
   (EConstr.isCast sigma x && is_Evar_or_CastedMeta sigma (pi1 (EConstr.destCast sigma x)))
 
 let occur_existential_or_casted_meta c =
-  let rec occrec c = match kind_of_term c with
+  let rec occrec c = match Constr.kind c with
     | Evar _ -> raise Not_found
     | Cast (m,_,_) when isMeta m -> raise Not_found
-    | _ -> iter_constr occrec c
+    | _ -> Constr.iter occrec c
   in try occrec c; false with Not_found -> true
 
 open Printer
@@ -84,12 +85,12 @@ let pf_find_abstract_proof check_lock gl abstract_n =
   let fire gl t = EConstr.Unsafe.to_constr (Reductionops.nf_evar (project gl) (EConstr.of_constr t)) in
   let abstract, gl = pf_mkSsrConst "abstract" gl in
   let l = Evd.fold_undefined (fun e ei l ->
-    match kind_of_term ei.Evd.evar_concl with
+    match Constr.kind ei.Evd.evar_concl with
     | App(hd, [|ty; n; lock|])
       when (not check_lock || 
                  (occur_existential_or_casted_meta  (fire gl ty) &&
                   is_Evar_or_CastedMeta (project gl) (EConstr.of_constr @@ fire gl lock))) &&
-      Term.eq_constr hd (EConstr.Unsafe.to_constr abstract) && Term.eq_constr n abstract_n -> e::l
+      Constr.equal hd (EConstr.Unsafe.to_constr abstract) && Constr.equal n abstract_n -> e::l
     | _ -> l) (project gl) [] in
   match l with
   | [e] -> e
@@ -286,7 +287,7 @@ let ssrabstract ist gens (*last*) gl =
             let p = mkApp (proj2,[|ty;concl;p|]) in
             let concl = mkApp(prod,[|ty; concl|]) in
             pf_unify_HO gl concl t, p
-        | App(hd, [|left; right|]) when Term.eq_constr hd prod ->
+        | App(hd, [|left; right|]) when Term.Constr.equal hd prod ->
             find_hole (mkApp (proj1,[|left;right;p|])) left
 *)
         | _ -> errorstrm(strbrk"abstract constant "++pr_econstr abstract_n++
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 507b4631b..36dce37ae 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -9,7 +9,8 @@
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
 open Names
-open Term
+module CoqConstr = Constr
+open CoqConstr
 open Termops
 open Constrexpr
 open Constrexpr_ops
@@ -364,7 +365,7 @@ let coerce_search_pattern_to_sort hpat =
 
 let interp_head_pat hpat =
   let filter_head, p = coerce_search_pattern_to_sort hpat in
-  let rec loop c = match kind_of_term c with
+  let rec loop c = match CoqConstr.kind c with
   | Cast (c', _, _) -> loop c'
   | Prod (_, _, c') -> loop c'
   | LetIn (_, _, _, c') -> loop c'
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index e3e34616b..d5c9e4988 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -18,10 +18,13 @@ let frozen_lexer = CLexer.get_keyword_state () ;;
 open Ltac_plugin
 open Names
 open Pp
-open Pcoq
 open Genarg
 open Stdarg
 open Term
+module CoqConstr = Constr
+open CoqConstr
+open Pcoq
+open Pcoq.Constr
 open Vars
 open Libnames
 open Tactics
@@ -35,10 +38,8 @@ open Evd
 open Tacexpr
 open Tacinterp
 open Pretyping
-open Constr
 open Ppconstr
 open Printer
-
 open Globnames
 open Misctypes
 open Decl_kinds
@@ -73,7 +74,7 @@ let pp s = !pp_ref s
 (** Utils {{{ *****************************************************************)
 let env_size env = List.length (Environ.named_context env)
 let safeDestApp c =
-  match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |]
+  match kind c with App (f, a) -> f, a | _ -> c, [| |]
 (* Toplevel constr must be globalized twice ! *)
 let glob_constr ist genv = function
   | _, Some ce ->
@@ -325,7 +326,7 @@ let unif_FO env ise p c =
 let nf_open_term sigma0 ise c =
   let c = EConstr.Unsafe.to_constr c in
   let s = ise and s' = ref sigma0 in
-  let rec nf c' = match kind_of_term c' with
+  let rec nf c' = match kind c' with
   | Evar ex ->
     begin try nf (existential_value s ex) with _ ->
     let k, a = ex in let a' = Array.map nf a in
@@ -333,7 +334,7 @@ let nf_open_term sigma0 ise c =
       s' := Evd.add !s' k (Evarutil.nf_evar_info s (Evd.find s k));
     mkEvar (k, a')
     end
-  | _ -> map_constr nf c' in
+  | _ -> map nf c' in
   let copy_def k evi () =
     if evar_body evi != Evd.Evar_empty then () else
     match Evd.evar_body (Evd.find s k) with
@@ -365,7 +366,7 @@ let pf_unify_HO gl t1 t2 =
   re_sig si sigma
 
 (* This is what the definition of iter_constr should be... *)
-let iter_constr_LR f c = match kind_of_term c with
+let iter_constr_LR f c = match kind c with
   | Evar (k, a) -> Array.iter f a
   | Cast (cc, _, t) -> f cc; f t  
   | Prod (_, t, b) | Lambda (_, t, b)  -> f t; f b
@@ -418,14 +419,14 @@ let all_ok _ _ = true
 let proj_nparams c =
   try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0
 
-let isRigid c = match kind_of_term c with
+let isRigid c = match kind c with
   | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true
   | _ -> false
 
 let hole_var = mkVar (Id.of_string "_")
 let pr_constr_pat c0 =
   let rec wipe_evar c =
-    if isEvar c then hole_var else map_constr wipe_evar c in
+    if isEvar c then hole_var else map wipe_evar c in
   pr_constr (wipe_evar c0)
 
 (* Turn (new) evars into metas *)
@@ -433,11 +434,11 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 =
   let ise = ref ise0 in
   let sigma = ref ise0 in
   let nenv = env_size env + if hack then 1 else 0 in
-  let rec put c = match kind_of_term c with
+  let rec put c = match kind c with
   | Evar (k, a as ex) ->
     begin try put (existential_value !sigma ex)
     with NotInstantiatedEvar ->
-    if Evd.mem sigma0 k then map_constr put c else
+    if Evd.mem sigma0 k then map put c else
     let evi = Evd.find !sigma k in
     let dc = List.firstn (max 0 (Array.length a - nenv)) (evar_filtered_context evi) in
     let abs_dc (d, c) = function
@@ -452,7 +453,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 =
     sigma := Evd.define k (applistc (mkMeta m) a) !sigma;
     put (existential_value !sigma ex)
     end
-  | _ -> map_constr put c in
+  | _ -> map put c in
   let c1 = put c0 in !ise, c1
 
 (* Compile a match pattern from a term; t is the term to fill. *)
@@ -462,7 +463,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
     let f, a = Reductionops.whd_betaiota_stack ise (EConstr.of_constr p) in
     let f = EConstr.Unsafe.to_constr f in
     let a = List.map EConstr.Unsafe.to_constr a in
-    match kind_of_term f with
+    match kind f with
     | Const (p,_) ->
       let np = proj_nparams p in
       if np = 0 || np > List.length a then KpatConst, f, a else
@@ -490,7 +491,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
 (* kind and arity for Proj and Flex patterns.                           *)
 let ungen_upat lhs (sigma, uc, t) u =
   let f, a = safeDestApp lhs in
-  let k = match kind_of_term f with
+  let k = match kind f with
   | Var _ | Ind _ | Construct _ -> KpatFixed
   | Const _ -> KpatConst
   | Evar (k, _) -> if is_defined sigma k then raise NoMatch else KpatEvar k
@@ -502,14 +503,14 @@ let ungen_upat lhs (sigma, uc, t) u =
 let nb_cs_proj_args pc f u =
   let na k =
     List.length (snd (lookup_canonical_conversion (ConstRef pc, k))).o_TCOMPS in
-  let nargs_of_proj t = match kind_of_term t with
+  let nargs_of_proj t = match kind t with
       | App(_,args) -> Array.length args
       | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be
                        the number of arguments including the projected *)
       | _ -> assert false in
-  try match kind_of_term f with
+  try match kind f with
   | Prod _ -> na Prod_cs
-  | Sort s -> na (Sort_cs (family_of_sort s))
+  | Sort s -> na (Sort_cs (Sorts.family s))
   | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f 
   | Proj (c',_) when Constant.equal (Projection.constant c') pc -> nargs_of_proj u.up_f
   | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f))
@@ -517,22 +518,22 @@ let nb_cs_proj_args pc f u =
   with Not_found -> -1
 
 let isEvar_k k f =
-  match kind_of_term f with Evar (k', _) -> k = k' | _ -> false
+  match kind f with Evar (k', _) -> k = k' | _ -> false
 
 let nb_args c =
-  match kind_of_term c with App (_, a) -> Array.length a | _ -> 0
+  match kind c with App (_, a) -> Array.length a | _ -> 0
 
 let mkSubArg i a = if i = Array.length a then a else Array.sub a 0 i
 let mkSubApp f i a = if i = 0 then f else mkApp (f, mkSubArg i a)
 
 let splay_app ise =
-  let rec loop c a = match kind_of_term c with
+  let rec loop c a = match kind c with
   | App (f, a') -> loop f (Array.append a' a)
   | Cast (c', _, _) -> loop c' a
   | Evar ex ->
     (try loop (existential_value ise ex) a with _ -> c, a)
   | _ -> c, a in
-  fun c -> match kind_of_term c with
+  fun c -> match kind c with
   | App (f, a) -> loop f a
   | Cast _ | Evar _ -> loop c [| |]
   | _ -> c, [| |]
@@ -541,8 +542,8 @@ let filter_upat i0 f n u fpats =
   let na = Array.length u.up_a in
   if n < na then fpats else
   let np = match u.up_k with
-  | KpatConst when Term.eq_constr u.up_f f -> na
-  | KpatFixed when Term.eq_constr u.up_f f -> na 
+  | KpatConst when equal u.up_f f -> na
+  | KpatFixed when equal u.up_f f -> na 
   | KpatEvar k when isEvar_k k f -> na
   | KpatLet when isLetIn f -> na
   | KpatLam when isLambda f -> na
@@ -554,7 +555,7 @@ let filter_upat i0 f n u fpats =
   if np < na then fpats else
   let () = if !i0 < np then i0 := n in (u, np) :: fpats
 
-let eq_prim_proj c t = match kind_of_term t with
+let eq_prim_proj c t = match kind t with
   | Proj(p,_) -> Constant.equal (Projection.constant p) c
   | _ -> false
 
@@ -562,13 +563,13 @@ let filter_upat_FO i0 f n u fpats =
   let np = nb_args u.up_FO in
   if n < np then fpats else
   let ok = match u.up_k with
-  | KpatConst -> Term.eq_constr u.up_f f 
-  | KpatFixed -> Term.eq_constr u.up_f f 
+  | KpatConst -> equal u.up_f f 
+  | KpatFixed -> equal u.up_f f 
   | KpatEvar k -> isEvar_k k f
   | KpatLet -> isLetIn f
   | KpatLam -> isLambda f
   | KpatRigid -> isRigid f
-  | KpatProj pc -> Term.eq_constr f (mkConst pc) || eq_prim_proj pc f
+  | KpatProj pc -> equal f (mkConst pc) || eq_prim_proj pc f
   | KpatFlex -> i0 := n; true in
   if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats
 
@@ -741,13 +742,13 @@ let mk_tpattern_matcher ?(all_instances=false)
       let x, pv, t, pb = destLetIn u.up_f in
       let env' =
         Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, t)) env in
-      let match_let f = match kind_of_term f with
+      let match_let f = match kind f with
       | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b
       | _ -> false in match_let
-    | KpatFixed -> Term.eq_constr u.up_f
-    | KpatConst -> Term.eq_constr u.up_f
+    | KpatFixed -> equal u.up_f
+    | KpatConst -> equal u.up_f
     | KpatLam -> fun c ->
-       (match kind_of_term c with
+       (match kind c with
        | Lambda _ -> unif_EQ env sigma u.up_f c
        | _ -> false)
     | _ -> unif_EQ env sigma u.up_f in
@@ -778,8 +779,8 @@ let rec uniquize = function
       let t1 = nf_evar sigma1 t1 in
       let f1 = nf_evar sigma1 f1 in
       let a1 = Array.map (nf_evar sigma1) a1 in
-      not (Term.eq_constr t t1 &&
-           Term.eq_constr f f1 && CArray.for_all2 Term.eq_constr a a1) in
+      not (equal t t1 &&
+           equal f f1 && CArray.for_all2 equal a a1) in
     x :: uniquize (List.filter neq xs) in
 
 ((fun env c h ~k -> 
@@ -1018,7 +1019,7 @@ let input_ssrtermkind strm = match stream_nth 0 strm with
   | Tok.KEYWORD "(" -> '('
   | Tok.KEYWORD "@" -> '@'
   | _ -> ' '
-let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
 let interp_ssrterm _ gl t = Tacmach.project gl, t
 
@@ -1100,7 +1101,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
   let decodeG t f g = decode ist (mkG t) f g in
   let bad_enc id _ = CErrors.anomaly (str"bad encoding for pattern "++str id++str".") in
   let cleanup_XinE h x rp sigma =
-    let h_k = match kind_of_term h with Evar (k,_) -> k | _ -> assert false in
+    let h_k = match kind h with Evar (k,_) -> k | _ -> assert false in
     let to_clean, update = (* handle rename if x is already used *)
       let ctx = pf_hyps gl in
       let len = Context.Named.length ctx in
@@ -1115,11 +1116,11 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
       with Not_found -> ref (Some x), fun _ -> () in
     let sigma0 = project gl in
     let new_evars =
-      let rec aux acc t = match kind_of_term t with
+      let rec aux acc t = match kind t with
       | Evar (k,_) ->
           if k = h_k || List.mem k acc || Evd.mem sigma0 k then acc else
           (update k; k::acc)
-      | _ -> fold_constr aux acc t in 
+      | _ -> CoqConstr.fold aux acc t in 
       aux [] (nf_evar sigma rp) in
     let sigma = 
       List.fold_left (fun sigma e ->
@@ -1202,7 +1203,7 @@ let interp_cpattern ist gl red redty = interp_pattern ist gl (T red) redty;;
 let interp_rpattern ~wit_ssrpatternarg ist gl red = interp_pattern ~wit_ssrpatternarg ist gl red None;;
 
 let id_of_pattern = function
-  | _, T t -> (match kind_of_term t with Var id -> Some id | _ -> None)
+  | _, T t -> (match kind t with Var id -> Some id | _ -> None)
   | _ -> None
 
 (* The full occurrence set *)
@@ -1222,7 +1223,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
       Evd.add (Evd.remove sigma e) e {e_def with Evd.evar_body = Evar_empty} in
     sigma, e_body in
   let ex_value hole =
-    match kind_of_term hole with Evar (e,_) -> e | _ -> assert false in
+    match kind hole with Evar (e,_) -> e | _ -> assert false in
   let mk_upat_for ?hack env sigma0 (sigma, t) ?(p=t) ok =
     let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in
     sigma, [pat] in
@@ -1407,7 +1408,7 @@ let () =
 
 let ssrinstancesof ist arg gl =
   let ok rhs lhs ise = true in
-(*   not (Term.eq_constr lhs (Evarutil.nf_evar ise rhs)) in *)
+(*   not (equal lhs (Evarutil.nf_evar ise rhs)) in *)
   let env, sigma, concl = pf_env gl, project gl, pf_concl gl in
   let concl = EConstr.Unsafe.to_constr concl in
   let sigma0, cpat = interp_cpattern ist gl arg None in
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 8e2a1a717..8ab666f7e 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -6,7 +6,7 @@ open Genarg
 open Tacexpr
 open Environ
 open Evd
-open Term
+open Constr
 
 (** ******** Small Scale Reflection pattern matching facilities ************* *)