aboutsummaryrefslogtreecommitdiff
path: root/checker/safe_checking.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-04-30 14:10:16 +0200
committerPierre-Marie Pédrot2020-04-30 14:10:16 +0200
commitd436c45a19de2f91aad94f492b547225f8c5b305 (patch)
treeb666e829b6545ba38170dcf79276714dd89cbe32 /checker/safe_checking.ml
parent010ef152611977770fa137ed5980205d412febe5 (diff)
parent7a4e7dfbaa8dc3fa92931c4bfa39d268940e08f8 (diff)
Merge PR #12107: Remove mod_constraints field of module body
Reviewed-by: ppedrot
Diffstat (limited to 'checker/safe_checking.ml')
-rw-r--r--checker/safe_checking.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
index 524ffbc022..b5beab532e 100644
--- a/checker/safe_checking.ml
+++ b/checker/safe_checking.ml
@@ -14,7 +14,7 @@ open Environ
let import senv 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 mb.mod_constraints env 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;