diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-07 08:34:29 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-07 08:34:29 +0000 |
| commit | 079edbff1af6f4be22d7a917522bd52651522640 (patch) | |
| tree | fec9ed4bac370ba442e2997e0d3a8c355685886f /kernel | |
| parent | d4af7ddf3585f6938ae24b72661965b1a00972ea (diff) | |
Mod_typing: fix the content of the typ_expr_alg field
Fix suggested by Elie. Without that, typ_expr_alg may contain
Foo instead of Bar when Foo is a module of type Bar.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13247 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/mod_typing.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index b2e199ff8..4b6b1ce5a 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -354,13 +354,14 @@ and translate_struct_type_entry env inl mse = match mse with and translate_module_type env mp inl mte = let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in - subst_modtype_and_resolver - {typ_mp = mp_from; - typ_expr = sign; - typ_expr_alg = alg; - typ_constraints = cst; - typ_delta = resolve} mp env - + let mtb = subst_modtype_and_resolver + {typ_mp = mp_from; + typ_expr = sign; + typ_expr_alg = None; + typ_constraints = cst; + typ_delta = resolve} mp env + in {mtb with typ_expr_alg = alg} + let rec translate_struct_include_module_entry env mp inl mse = match mse with | MSEident mp1 -> let mb = lookup_module mp1 env in |