From dd96b1e5e8d0eb9f93cff423b6f9cf900aee49d7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 30 May 2014 20:55:48 +0200
Subject: - Fix hashing of levels to get the "right" order in universe contexts
 etc... - Add a tentative syntax for specifying universes: Type{"i"} and
 foo@{Type{"i"},Type{"j"}}. These are always rigid. - Use level-to-level
 substitutions where the more general level-to-universe substitutions were
 previously used.

---
 printing/ppconstr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 950594397a..019fad0ce8 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -119,7 +119,7 @@ let pr_qualid = pr_qualid
 let pr_patvar = pr_id
 
 let pr_universe_instance l =
-  pr_opt (pr_in_comment Univ.Instance.pr) l
+  pr_opt (pr_in_comment (prlist_with_sep spc pr_glob_sort)) l
 
 let pr_cref ref us =
   pr_reference ref ++ pr_universe_instance us
-- 
cgit v1.2.3