diff options
Diffstat (limited to 'checker/safe_checking.ml')
| -rw-r--r-- | checker/safe_checking.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml index b5beab532e..55bfa36ce5 100644 --- a/checker/safe_checking.ml +++ b/checker/safe_checking.ml @@ -11,14 +11,14 @@ open Declarations open Environ -let import senv clib univs digest = +let import senv opac clib univs digest = let mb = Safe_typing.module_of_library clib in let env = Safe_typing.env_of_safe_env senv in let env = push_context_set ~strict:true (Safe_typing.univs_of_library clib) env in let env = push_context_set ~strict:true univs env in let env = Modops.add_retroknowledge mb.mod_retroknowledge env in - Mod_checking.check_module env mb.mod_mp mb; - let (_,senv) = Safe_typing.import clib univs digest senv in senv + let opac = Mod_checking.check_module env opac mb.mod_mp mb in + let (_,senv) = Safe_typing.import clib univs digest senv in senv, opac let unsafe_import senv clib univs digest = let (_,senv) = Safe_typing.import clib univs digest senv in senv |