aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--checker/safe_typing.ml2
-rw-r--r--kernel/safe_typing.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 5e7d7f42f8..5986281667 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -100,7 +100,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 =
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 =