aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/univ.ml')
-rw-r--r--kernel/univ.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 064dde3a6..6c2316988 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1768,7 +1768,7 @@ struct
let pr prl (univs, cst as ctx) =
if is_empty ctx then mt() else
- Instance.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst)
+ h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
let hcons (univs, cst) =
(Instance.hcons univs, hcons_constraints cst)
@@ -1842,7 +1842,7 @@ struct
let pr prl (univs, cst as ctx) =
if is_empty ctx then mt() else
- LSet.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst)
+ h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
let constraints (univs, cst) = cst
let levels (univs, cst) = univs