diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-31 17:02:00 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-31 17:02:00 +0100 |
| commit | 5319465eb1eaf89410dac96cd14b14b9b95601e7 (patch) | |
| tree | b52306041b4351e6a01984d391da3a82af82ec11 /kernel/safe_typing.ml | |
| parent | 1a157442dff4bfa127af467c49280e79889acde7 (diff) | |
| parent | d3bc575c498ae09ad1003405d17a9d5cfbcf3cbf (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f86fdfa97..c7ab6491d 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -748,7 +748,7 @@ let end_modtype l senv = let add_include me is_module inl senv = let open Mod_typing in let mp_sup = senv.modpath in - let sign,_,resolver,cst = + let sign,(),resolver,cst = translate_mse_incl is_module senv.env mp_sup inl me in let senv = add_constraints (Now (false, cst)) senv in |