summaryrefslogtreecommitdiff
path: root/checker/mod_checking.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r--checker/mod_checking.ml9
1 files changed, 8 insertions, 1 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index af5e4f46..9e7a2336 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -130,6 +130,12 @@ let check_definition_sub env cb1 cb2 =
Reduction.conv env c1 c2
| _ -> ())
+let lookup_modtype mp env =
+ try Environ.lookup_modtype mp env
+ with Not_found ->
+ failwith ("Unknown module type: "^string_of_mp mp)
+
+
let rec check_with env mtb with_decl =
match with_decl with
| With_definition_body _ ->
@@ -308,7 +314,8 @@ and check_structure_field (s,env) mp lab = function
and check_modexpr env mse = match mse with
| SEBident mp ->
- let mtb = lookup_modtype mp env in
+ let mp = scrape_alias mp env in
+ let mtb = lookup_modtype mp env in
mtb.typ_alias
| SEBfunctor (arg_id, mtb, body) ->
check_module_type env mtb;