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 | |
| 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')
| -rw-r--r-- | printing/ppconstr.ml | 6 | ||||
| -rw-r--r-- | printing/ppconstrsig.mli | 1 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 3 |
3 files changed, 9 insertions, 1 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 diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli index a59fc6d67d..3de0d805c4 100644 --- a/printing/ppconstrsig.mli +++ b/printing/ppconstrsig.mli @@ -44,6 +44,7 @@ module type Pp = sig val pr_qualid : qualid -> std_ppcmds val pr_patvar : patvar -> std_ppcmds + val pr_glob_level : glob_level -> std_ppcmds val pr_glob_sort : glob_sort -> std_ppcmds val pr_guard_annot : (constr_expr -> std_ppcmds) -> local_binder list -> diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 503b29aaf2..2d87b51d73 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -838,7 +838,8 @@ module Make ) | VernacConstraint v -> let pr_uconstraint (l, d, r) = - pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r + pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ + pr_glob_level r in return ( hov 2 (keyword "Constraint" ++ spc () ++ |