From 88afd8a9853c772b6b1681c7ae208e55e7daacbe Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sun, 19 Nov 2017 08:11:07 +0100
Subject: [api] Deprecate Term destructors, move to Constr

We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.

This is a step towards having a single module for `Constr`.
---
 plugins/cc/ccalgo.ml | 16 ++++++++--------
 plugins/cc/cctac.ml  |  1 -
 2 files changed, 8 insertions(+), 9 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index faabd7c14..ccef9ab96 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -12,13 +12,13 @@
 
 open CErrors
 open Pp
-open Goptions
 open Names
-open Term
+open Sorts
 open Constr
 open Vars
-open Tacmach
 open Evd
+open Goptions
+open Tacmach
 open Util
 
 let init_size=5
@@ -437,7 +437,7 @@ and make_app l=function
 and applist_proj c l =
   match c with
   | Symb s -> applist_projection s l
-  | _ -> applistc (constr_of_term c) l
+  | _ -> Term.applistc (constr_of_term c) l
 and applist_projection c l =
   match Constr.kind c with
   | Const c when Environ.is_projection (fst c) (Global.env()) ->
@@ -447,10 +447,10 @@ and applist_projection c l =
       let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *)
       let pb = Environ.lookup_projection p (Global.env()) in
       let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in
-	it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
+      Term.it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
     | hd :: tl ->
-      applistc (mkProj (p, hd)) tl)
-  | _ -> applistc c l
+      Term.applistc (mkProj (p, hd)) tl)
+  | _ -> Term.applistc c l
 
 let rec canonize_name sigma c =
   let c = EConstr.Unsafe.to_constr c in
@@ -838,7 +838,7 @@ let complete_one_class state i=
 	let _args =
 	  List.map (fun i -> constr_of_term (term state.uf  i))
 	    pac.args in
-	let typ = prod_applist _c (List.rev _args) in
+        let typ = Term.prod_applist _c (List.rev _args) in
 	let ct = app (term state.uf i) typ pac.arity in
 	  state.uf.epsilons <- pac :: state.uf.epsilons;
 	  ignore (add_term state ct)
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7dec34d4d..8642df684 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -12,7 +12,6 @@ open Evd
 open Names
 open Inductiveops
 open Declarations
-open Term
 open Constr
 open EConstr
 open Vars
-- 
cgit v1.2.3