diff options
| author | Matthieu Sozeau | 2014-06-10 13:08:48 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-10 13:08:48 +0200 |
| commit | f02823d9f6de5a8e5706c8433b6e2445cb50222f (patch) | |
| tree | a1abe9869258302bb165e7385334f5bc74a4d818 /printing | |
| parent | 80b589e91fe4c6e6e390132633557dc04b9c533a (diff) | |
Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Universes.
Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 22c89af8aa..3369e658b4 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -108,12 +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_univ_annot 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_no_spc (pr_in_braces str) u) + | GType u -> hov 0 (str "Type" ++ pr_opt_no_spc (pr_univ_annot str) u) let pr_id = pr_id let pr_name = pr_name @@ -129,8 +129,7 @@ let pr_glob_sort_instance = function | None -> str "Type") let pr_universe_instance l = - pr_opt_no_spc (fun i -> - str"@" ++ pr_in_braces (prlist_with_sep spc pr_glob_sort_instance) i) l + pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l let pr_cref ref us = pr_reference ref ++ pr_universe_instance us |