diff options
| author | Maxime Dénès | 2016-09-30 12:51:16 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-30 12:51:16 +0200 |
| commit | 7543449792d417a92092b692986d62b622b78ffc (patch) | |
| tree | 8244b6c3efa88abe12ab990a4ae4b3d0af8f5dc1 /printing/ppconstr.ml | |
| parent | bff880ffb6ef33c99a96e7925c995b31b1497e6a (diff) | |
| parent | 9615c025a2a09b69f2001d44a66a1fddef74e680 (diff) | |
Merge remote-tracking branch 'github/pr/299' into v8.6
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in
constraints.
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index a00e4bab30..aa0ebbb83b 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -149,6 +149,12 @@ end) = struct | GType [] -> tag_type (str "Type") | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u) + let pr_glob_level = function + | GProp -> tag_type (str "Prop") + | GSet -> tag_type (str "Set") + | GType None -> tag_type (str "Type") + | GType (Some (_, u)) -> tag_type (str u) + let pr_qualid sp = let (sl, id) = repr_qualid sp in let id = tag_ref (pr_id id) in |