aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/modops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/modops.ml')
-rw-r--r--kernel/modops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml
index daee0f187..58ebb4ad7 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -210,7 +210,7 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body ->
in
let ty' = subst_signature sub do_delta ty in
let me' = subst_impl sub me in
- let aty' = Option.smartmap (subst_expression sub id_delta) aty in
+ let aty' = Option.Smart.map (subst_expression sub id_delta) aty in
let delta' = do_delta mb.mod_delta sub in
if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta
then mb