diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-09-29 15:51:18 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-09-29 15:56:10 +0200 |
| commit | 9615c025a2a09b69f2001d44a66a1fddef74e680 (patch) | |
| tree | 4643d4f0f38b89402265df46c56119e28a8afe40 /printing/ppconstr.ml | |
| parent | 5348a615a484e379896deac8a6944af1f92b2d4c (diff) | |
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 a00e4bab3..aa0ebbb83 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 |