aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/safe_typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/safe_typing.ml')
-rw-r--r--checker/safe_typing.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index d3bc8373a..81a3cc035 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -28,7 +28,7 @@ let set_engagement c =
let full_add_module dp mb univs digest =
let env = !genv in
let env = push_context_set ~strict:true mb.mod_constraints env in
- let env = add_constraints univs env in
+ let env = push_context_set ~strict:true univs env in
let env = Modops.add_module mb env in
genv := add_digest env dp digest
@@ -83,7 +83,7 @@ let import file clib univs digest =
check_engagement env clib.comp_enga;
let mb = clib.comp_mod in
Mod_checking.check_module
- (add_constraints univs
+ (push_context_set ~strict:true univs
(push_context_set ~strict:true mb.mod_constraints env)) mb.mod_mp mb;
stamp_library file digest;
full_add_module clib.comp_name mb univs digest