aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r--kernel/safe_typing.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 91e4c73fc..f7f6a980d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -329,7 +329,7 @@ let start_module l senv =
let end_module l restype senv =
let oldsenv = senv.old in
let modinfo = senv.modinfo in
- let restype = option_map (translate_modtype senv.env) restype in
+ let restype = Option.map (translate_modtype senv.env) restype in
let params =
match modinfo.variant with
| NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
@@ -633,9 +633,9 @@ let import (dp,mb,depends,engmt) digest senv =
let rec lighten_module mb =
{ mb with
- mod_expr = option_map lighten_modexpr mb.mod_expr;
+ mod_expr = Option.map lighten_modexpr mb.mod_expr;
mod_type = lighten_modtype mb.mod_type;
- mod_user_type = option_map lighten_modtype mb.mod_user_type }
+ mod_user_type = Option.map lighten_modtype mb.mod_user_type }
and lighten_modtype = function
| MTBident kn as x -> x