diff options
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 383f7c2c95..9f03b57c5d 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -249,8 +249,10 @@ and check_modtypes cst env mtb1 mtb2 equiv = add_module (MPbound arg_id2) (module_body_of_type arg_t2) env in let body_t1' = + (* since we are just checking well-typedness we do not need + to expand any constant. Hence the identity resolver. *) subst_modtype - (map_mbid arg_id1 (MPbound arg_id2)) + (map_mbid arg_id1 (MPbound arg_id2) None) body_t1 in check_modtypes cst env' body_t1' body_t2 equiv |