diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:27:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:46:52 +0100 |
| commit | 03e21974a3e971a294533bffb81877dc1bd270b6 (patch) | |
| tree | 1b37339378f6bc93288b61f707efb6b08f992dc5 /kernel/cClosure.ml | |
| parent | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff) | |
[api] Move structures deprecated in the API to the core.
We do up to `Term` which is the main bulk of the changes.
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 12 |
1 files changed, 6 insertions, 6 deletions
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) -> |