Checker now disables VM and native

At the same time, we made the safe_env threading explicit.

1 files changed, 6 insertions, 5 deletions

diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
index 90b5188d26..6dc2953060 100644
--- a/checker/safe_checking.ml
+++ b/checker/safe_checking.ml
@@ -11,12 +11,13 @@
 open Declarations
 open Environ
 
-let import clib univs digest =
+let import senv clib univs digest =
   let mb = Safe_typing.module_of_library clib in
-  let env = push_context_set ~strict:true mb.mod_constraints (Global.env ())  in
+  let env = Safe_typing.env_of_safe_env senv in
+  let env = push_context_set ~strict:true mb.mod_constraints env in
   let env = push_context_set ~strict:true univs env in
   Mod_checking.check_module env mb.mod_mp mb;
-  let _ = Global.import clib univs digest in ()
+  let (_,senv) = Safe_typing.import clib univs digest senv in senv
 
-let unsafe_import clib univs digest =
-  let _ = Global.import clib univs digest in ()
+let unsafe_import senv clib univs digest =
+  let (_,senv) = Safe_typing.import clib univs digest senv in senv