diff options
| author | Gaëtan Gilbert | 2020-04-16 23:06:35 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-20 13:19:17 +0200 |
| commit | 7a4e7dfbaa8dc3fa92931c4bfa39d268940e08f8 (patch) | |
| tree | 13c841f5e345bc11b4ed78af0f51b8a087890fbe /plugins | |
| parent | e77b7aed145718b73ca58c75bc7ed01d2b55446f (diff) | |
Remove mod_constraints field of module body
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 02383799a9..f7d78551d8 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -163,7 +163,8 @@ let expand_mexpr env mpo me = let expand_modtype env mp me = let inl = Some (Flags.get_inline_level()) in - Mod_typing.translate_modtype env mp inl ([],me) + let mtb, _cst = Mod_typing.translate_modtype env mp inl ([],me) in + mtb let no_delta = Mod_subst.empty_delta_resolver |