From 209faf81c432c39d4537f8b1dc5c9947d4349d30 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 4 Nov 2015 14:35:02 -0500
Subject: Univs: update refman, better printers for universe contexts.

---
 kernel/univ.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 064dde3a64..6c2316988e 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
-- 
cgit v1.2.3