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

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

5 files changed, 15 insertions, 13 deletions

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