aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelibrary.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativelibrary.ml')
-rw-r--r--kernel/nativelibrary.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index f33e1eaa6..ddd795917 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -47,13 +47,13 @@ and translate_field prefix mp env acc (l,x) =
Pp.msg_debug (Pp.str msg));
translate_mod prefix mp env md.mod_type acc
| SFBmodtype mdtyp ->
- let mp = mdtyp.typ_mp in
+ let mp = mdtyp.mod_mp in
(if !Flags.debug then
let msg =
Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
in
Pp.msg_debug (Pp.str msg));
- translate_mod prefix mp env mdtyp.typ_expr acc
+ translate_mod prefix mp env mdtyp.mod_type acc
let dump_library mp dp env mod_expr =
if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library...");