From dbada2989e334756971c7bf69578c93b2e45643e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 4 Jun 2014 17:18:58 +0200
Subject: - Better parsing and printing of named universes: Type{ident} and
 foo@{(ident|Prop|Set|Type|' ')*} (user given names are still write only). -
 Add test-suite file for named universes.

---
 printing/ppconstr.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'printing/ppconstr.ml')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 5b6c072839..22c89af8aa 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -108,10 +108,12 @@ let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
 
 let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
 
+let pr_in_braces pr x = str "{" ++ pr x ++ str "}"
+
 let pr_glob_sort = function
   | GProp -> str "Prop"
   | GSet -> str "Set"
-  | GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment str) u)
+  | GType u -> hov 0 (str "Type" ++ pr_opt_no_spc (pr_in_braces str) u)
 
 let pr_id = pr_id
 let pr_name = pr_name
@@ -127,7 +129,8 @@ let pr_glob_sort_instance = function
     | None -> str "Type")
 
 let pr_universe_instance l =
-  pr_opt (pr_in_comment (prlist_with_sep spc pr_glob_sort_instance)) l
+  pr_opt_no_spc (fun i -> 
+    str"@" ++ pr_in_braces (prlist_with_sep spc pr_glob_sort_instance) i) l
 
 let pr_cref ref us =
   pr_reference ref ++ pr_universe_instance us
-- 
cgit v1.2.3