aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-05-23 18:23:28 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-05-23 18:50:10 +0200
commitbb2d7f94ba8688f57dc62ca72a857b82368aa784 (patch)
tree5282ed7a0038ce0babbfc1b8b94eefa870707be8 /checker
parent33b5074f24270c202a9922f21d445c12cc6b3b3d (diff)
Moving Option.smart_map to Option.Smart.map.
Diffstat (limited to 'checker')
-rw-r--r--checker/declarations.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 3368d68f7..ddd505a9a 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -599,7 +599,7 @@ and subst_body : 'a. (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generi
mod_mp = subst_mp sub mb.mod_mp;
mod_expr = subst_impl sub mb.mod_expr;
mod_type = subst_signature sub mb.mod_type;
- mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg }
+ mod_type_alg = Option.Smart.map (subst_expression sub) mb.mod_type_alg }
and subst_module sub mb =
subst_body (fun sub e -> implem_map (subst_signature sub) (subst_expression sub) e) sub mb