aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/printer.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml
index 1ad9dba499..374b5d597b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -640,7 +640,7 @@ let print_constructors envpar names types =
let pc =
prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
(fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c)
- (Array.to_list (array_map2 (fun n t -> (n,t)) names types))
+ (Array.to_list (Array.map2 (fun n t -> (n,t)) names types))
in
hv 0 (str " " ++ pc)