diff options
| -rw-r--r-- | kernel/modops.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 8febff5e8..97697f5de 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -144,11 +144,13 @@ let rec subst_with_body sub = function and subst_modtype sub mtb = let typ_expr' = subst_struct_expr sub mtb.typ_expr in - if typ_expr'==mtb.typ_expr then + let sub_mtb = join_alias mtb.typ_alias sub in + if typ_expr'==mtb.typ_expr && sub_mtb==mtb.typ_alias then mtb else { mtb with - typ_expr = typ_expr'} + typ_expr = typ_expr'; + typ_alias = sub_mtb} and subst_structure sub sign = let subst_body = function |