aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/safe_typing.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 504bfab04b..43090c8e10 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -866,7 +866,7 @@ end = struct
let traverse_library on_opaque_const_body =
let rec lighten_module mb =
{ mb with
- mod_expr = None;
+ mod_expr = Option.map lighten_modexpr mb.mod_expr;
mod_type = lighten_modexpr mb.mod_type;
}
and lighten_struct struc =