diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-16 14:14:28 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-16 14:14:28 +0000 |
| commit | 456ff087953a62df0b46e76f16d0117363558b0d (patch) | |
| tree | 2cec913f9689e6410c0ecebe3d95b076464cd942 /kernel/mod_typing.ml | |
| parent | d31d8723b5b103b4937c63dd2560c07b04492a3a (diff) | |
cf. 12945
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12946 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index cfa256888..c9d9ac924 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -361,7 +361,8 @@ let rec translate_struct_include_module_entry env mp inl mse = match mse with | MSEident mp1 -> let mb = lookup_module mp1 env in let mb' = strengthen_and_subst_mb mb mp env true in - mb'.mod_type, mb'.mod_delta,Univ.Constraint.empty + let mb_typ = clean_bounded_mod_expr mb'.mod_type in + mb_typ, mb'.mod_delta,Univ.Constraint.empty | MSEapply (fexpr,mexpr) -> let sign,resolver,cst1 = translate_struct_include_module_entry env mp inl fexpr in |