From b053d98fb17d2f46878f49d7adf4839ae632c10b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 15 May 2018 21:51:21 +0200
Subject: Remove vm_conv hook and reorganize kernel files

---
 kernel/nativeconv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativeconv.ml')

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index c71f746bec..f51b583225 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -163,7 +163,7 @@ let warn_no_native_compiler =
 let native_conv cv_pb sigma env t1 t2 =
   if not Coq_config.native_compiler then begin
     warn_no_native_compiler ();
-    vm_conv cv_pb env t1 t2
+    Vconv.vm_conv cv_pb env t1 t2
   end
   else
   let univs = Environ.universes env in
-- 
cgit v1.2.3


From 4552729b88058946055dddde1533057e25bfc5a9 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 16 May 2018 00:06:51 +0200
Subject: Unify pre_env and env

We now have only two notions of environments in the kernel: env and
safe_env.
---
 kernel/nativeconv.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'kernel/nativeconv.ml')

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index f51b583225..c07025660e 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -136,9 +136,8 @@ and conv_fix env lvl t1 f1 t2 f2 cu =
   aux 0 cu
 
 let native_conv_gen pb sigma env univs t1 t2 =
-  let penv = Environ.pre_env env in 
   let ml_filename, prefix = get_ml_filename () in
-  let code, upds = mk_conv_code penv sigma prefix t1 t2 in
+  let code, upds = mk_conv_code env sigma prefix t1 t2 in
   match compile ml_filename code ~profile:false with
   | (true, fn) ->
       begin
-- 
cgit v1.2.3