From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 6 Nov 2017 23:27:09 +0100
Subject: [api] Move structures deprecated in the API to the core.

We do up to `Term` which is the main bulk of the changes.
---
 kernel/cClosure.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'kernel/cClosure.ml')

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index e8cce0841..e1b086b75 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -23,7 +23,7 @@ open CErrors
 open Util
 open Pp
 open Names
-open Term
+open Constr
 open Vars
 open Environ
 open Esubst
@@ -516,7 +516,7 @@ let zupdate m s =
   else s
 
 let mk_lambda env t =
-  let (rvars,t') = decompose_lam t in
+  let (rvars,t') = Term.decompose_lam t in
   FLambda(List.length rvars, List.rev rvars, t', env)
 
 let destFLambda clos_fun t =
@@ -530,7 +530,7 @@ let destFLambda clos_fun t =
 (* Optimization: do not enclose variables in a closure.
    Makes variable access much faster *)
 let mk_clos e t =
-  match kind_of_term t with
+  match kind t with
     | Rel i -> clos_rel e i
     | Var x -> { norm = Red; term = FFlex (VarKey x) }
     | Const c -> { norm = Red; term = FFlex (ConstKey c) }
@@ -556,7 +556,7 @@ let mk_clos_vect env v = match v with
    subterms.
    Could be used insted of mk_clos. *)
 let mk_clos_deep clos_fun env t =
-  match kind_of_term t with
+  match kind t with
     | (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) ->
         mk_clos env t
     | Cast (a,k,b) ->
@@ -655,7 +655,7 @@ let term_of_fconstr =
     match v.term with
       | FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t
       | FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts ->
-          compose_lam (List.rev tys) f
+          Term.compose_lam (List.rev tys) f
       | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> mkFix fx
       | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> mkCoFix cfx
       | _ -> to_constr term_of_fconstr_lift lfts v in
@@ -891,7 +891,7 @@ let rec knh info m stk =
 
 (* The same for pure terms *)
 and knht info e t stk =
-  match kind_of_term t with
+  match kind t with
     | App(a,b) ->
         knht info e a (append_stack (mk_clos_vect e b) stk)
     | Case(ci,p,t,br) ->
-- 
cgit v1.2.3