aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/genarg.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/genarg.ml')
-rw-r--r--interp/genarg.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 930cfe739..fc93f455a 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -223,7 +223,7 @@ let app_list1 f = function
let app_opt f = function
| (OptArgType t as u, l) ->
let o = Obj.magic l in
- (u, Obj.repr (option_map (fun x -> out_gen t (f (in_gen t x))) o))
+ (u, Obj.repr (Option.map (fun x -> out_gen t (f (in_gen t x))) o))
| _ -> failwith "Genarg: not an opt"
let app_pair f1 f2 = function