aboutsummaryrefslogtreecommitdiff
path: root/printing/ppconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/ppconstr.ml')
-rw-r--r--printing/ppconstr.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 650b8f7262..ea705e335e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -140,8 +140,8 @@ end) = struct
let pr_univ l =
match l with
- | [x] -> str x
- | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")"
+ | [_,x] -> str x
+ | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")"
let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
@@ -174,7 +174,7 @@ end) = struct
tag_type (str "Set")
| GType u ->
(match u with
- | Some u -> str u
+ | Some (_,u) -> str u
| None -> tag_type (str "Type"))
let pr_universe_instance l =