Remove (useless) aliases from the API.

3 files changed, 16 insertions, 16 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index e8589f2ce..5c7cad7ff 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -136,7 +136,7 @@ let family_eq f1 f2 = match f1, f2 with
 
 type term=
     Symb of constr
-  | Product of sorts * sorts
+  | Product of Sorts.t * Sorts.t
   | Eps of Id.t
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
@@ -270,7 +270,7 @@ type state =
      mutable rew_depth:int;
      mutable changed:bool;
      by_type: Int.Set.t Typehash.t;
-     mutable gls:Proof_type.goal Tacmach.sigma}
+     mutable gls:Proof_type.goal Evd.sigma}
 
 let dummy_node =
   {
@@ -457,13 +457,13 @@ let rec canonize_name sigma c =
   let func c = canonize_name sigma (EConstr.of_constr c) in
     match kind_of_term c with
       | Const (kn,u) ->
-	  let canon_const = constant_of_kn (canonical_con kn) in 
+	  let canon_const = Constant.make1 (Constant.canonical kn) in 
 	    (mkConstU (canon_const,u))
       | Ind ((kn,i),u) ->
-	  let canon_mind = mind_of_kn (canonical_mind kn) in
+	  let canon_mind = MutInd.make1 (MutInd.canonical kn) in
 	    (mkIndU ((canon_mind,i),u))
       | Construct (((kn,i),j),u) ->
-	  let canon_mind = mind_of_kn (canonical_mind kn) in
+	  let canon_mind = MutInd.make1 (MutInd.canonical kn) in
 	    mkConstructU (((canon_mind,i),j),u)
       | Prod (na,t,ct) ->
 	  mkProd (na,func t, func ct)
@@ -475,7 +475,7 @@ let rec canonize_name sigma c =
 	  mkApp (func ct,Array.smartmap func l)
       | Proj(p,c) ->
 	let p' = Projection.map (fun kn ->
-          constant_of_kn (canonical_con kn)) p in 
+          Constant.make1 (Constant.canonical kn)) p in 
 	  (mkProj (p', func c))
       | _ -> c
 
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 871de7253..505029992 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -31,7 +31,7 @@ type cinfo =
 
 type term =
     Symb of constr
-  | Product of sorts * sorts
+  | Product of Sorts.t * Sorts.t
   | Eps of Id.t
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
@@ -129,7 +129,7 @@ val axioms : forest -> (term * term) Constrhash.t
 
 val epsilons : forest -> pa_constructor list
 
-val empty : int -> Proof_type.goal Tacmach.sigma -> state
+val empty : int -> Proof_type.goal Evd.sigma -> state
 
 val add_term : state -> term -> int
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index e8b2d7615..1ce1660b3 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -66,7 +66,7 @@ let rec decompose_term env sigma t=
     | Construct c ->
 	let (((mind,i_ind),i_con),u)= c in 
 	let u = EInstance.kind sigma u in
-	let canon_mind = mind_of_kn (canonical_mind mind) in
+	let canon_mind = MutInd.make1 (MutInd.canonical mind) in
 	let canon_ind = canon_mind,i_ind in
 	let (oib,_)=Global.lookup_inductive (canon_ind) in
 	let nargs=constructor_nallargs_env env (canon_ind,i_con) in
@@ -76,16 +76,16 @@ let rec decompose_term env sigma t=
     | Ind c -> 
 	let (mind,i_ind),u = c in 
 	let u = EInstance.kind sigma u in
-	let canon_mind = mind_of_kn (canonical_mind mind) in
-	let canon_ind = canon_mind,i_ind in  (Symb (Constr.mkIndU (canon_ind,u)))
+	let canon_mind = MutInd.make1 (MutInd.canonical mind) in
+	let canon_ind = canon_mind,i_ind in  (Symb (Term.mkIndU (canon_ind,u)))
     | Const (c,u) -> 
 	let u = EInstance.kind sigma u in
-	let canon_const = constant_of_kn (canonical_con c) in 
-	  (Symb (Constr.mkConstU (canon_const,u)))
+	let canon_const = Constant.make1 (Constant.canonical c) in 
+	  (Symb (Term.mkConstU (canon_const,u)))
     | Proj (p, c) -> 
-	let canon_const kn = constant_of_kn (canonical_con kn) in 
+	let canon_const kn = Constant.make1 (Constant.canonical kn) in 
 	let p' = Projection.map canon_const p in
-	(Appli (Symb (Constr.mkConst (Projection.constant p')), decompose_term env sigma c))
+	(Appli (Symb (Term.mkConst (Projection.constant p')), decompose_term env sigma c))
     | _ ->
        let t = Termops.strip_outer_cast sigma t in
        if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found
@@ -198,7 +198,7 @@ let make_prb gls depth additionnal_terms =
       (fun decl ->
          let id = NamedDecl.get_id decl in
 	 begin
-	   let cid=Constr.mkVar id in
+	   let cid=Term.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