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/nativelambda.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'kernel/nativelambda.ml')

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)))
-- 
cgit v1.2.3