diff options
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 28 |
1 files changed, 16 insertions, 12 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 315571705..9942816d1 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -253,18 +253,22 @@ and check_module env mp mb = let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in let (_:struct_expr_body) = check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in - check_subtypes env - {typ_mp=mp; - typ_expr=sign; - typ_expr_alg=None; - typ_constraints=Univ.empty_constraint; - typ_delta = mb.mod_delta;} - {typ_mp=mp; - typ_expr=mb.mod_type; - typ_expr_alg=None; - typ_constraints=Univ.empty_constraint; - typ_delta = mb.mod_delta;}; - + let mtb1 = + {typ_mp=mp; + typ_expr=sign; + typ_expr_alg=None; + typ_constraints=Univ.empty_constraint; + typ_delta = mb.mod_delta;} + and mtb2 = + {typ_mp=mp; + typ_expr=mb.mod_type; + typ_expr_alg=None; + typ_constraints=Univ.empty_constraint; + typ_delta = mb.mod_delta;} + in + let env = add_module (module_body_of_type mp mtb1) env in + check_subtypes env mtb1 mtb2 + and check_structure_field env mp lab res = function | SFBconst cb -> let c = make_con mp empty_dirpath lab in |