diff options
| author | Pierre-Marie Pédrot | 2020-04-30 14:10:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-30 14:10:16 +0200 |
| commit | d436c45a19de2f91aad94f492b547225f8c5b305 (patch) | |
| tree | b666e829b6545ba38170dcf79276714dd89cbe32 /checker/safe_checking.ml | |
| parent | 010ef152611977770fa137ed5980205d412febe5 (diff) | |
| parent | 7a4e7dfbaa8dc3fa92931c4bfa39d268940e08f8 (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.ml | 2 |
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; |
