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/nativelambda.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/nativelambda.ml')
-rw-r--r-- | kernel/nativelambda.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index aaa9f9b00..de4dc2107 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -8,7 +8,7 @@ open Util open Names open Esubst -open Term +open Constr open Declarations open Pre_env open Nativevalues @@ -417,9 +417,9 @@ module Renv = (* What about pattern matching ?*) let is_lazy prefix t = - match kind_of_term t with + match kind t with | App (f,args) -> - begin match kind_of_term f with + begin match kind f with | Construct (c,_) -> let entry = mkInd (fst c) in (try @@ -448,7 +448,7 @@ let empty_evars = let empty_ids = [||] let rec lambda_of_constr env sigma c = - match kind_of_term c with + match kind c with | Meta mv -> let ty = meta_type sigma mv in Lmeta (mv, lambda_of_constr env sigma ty) @@ -480,7 +480,7 @@ let rec lambda_of_constr env sigma c = Lprod(ld, Llam([|id|], lc)) | Lambda _ -> - let params, body = decompose_lam c in + let params, body = Term.decompose_lam c in let ids = get_names (List.rev params) in Renv.push_rels env ids; let lb = lambda_of_constr env sigma body in @@ -561,7 +561,7 @@ let rec lambda_of_constr env sigma c = Lcofix(init, (names, ltypes, lbodies)) and lambda_of_app env sigma f args = - match kind_of_term f with + match kind f with | Const (kn,u as c) -> let kn,u = get_alias !global_env c in let cb = lookup_constant kn !global_env in @@ -656,7 +656,7 @@ let compile_static_int31 fc args = if not fc then raise Not_found else Luint (UintVal (Uint31.of_int (Array.fold_left - (fun temp_i -> fun t -> match kind_of_term t with + (fun temp_i -> fun t -> match kind t with | Construct ((_,d),_) -> 2*temp_i+d-1 | _ -> raise NotClosed) 0 args))) |