diff options
| author | Matthieu Sozeau | 2014-07-01 22:50:37 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-01 22:52:08 +0200 |
| commit | 4c97e4ce19ca4c387039cfdcb4f24658100230b0 (patch) | |
| tree | 8e6367b1936d842b3e56283abc25de2342452884 /printing/ppvernac.ml | |
| parent | 3d2582eeb492fb21b7136016bf4c1a0463dc15c2 (diff) | |
Add toplevel commands to declare global universes and constraints.
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index d89731147b..f088477e79 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -691,7 +691,15 @@ let rec pr_vernac = function hov 2 (str"Combined Scheme" ++ spc() ++ pr_lident id ++ spc() ++ str"from" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l) - + | VernacUniverse v -> + hov 2 (str"Universe" ++ spc () ++ + prlist_with_sep (fun _ -> str",") pr_lident v) + | VernacConstraint v -> + let pr_uconstraint (l, d, r) = + pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r + in + hov 2 (str"Constraint" ++ spc () ++ + prlist_with_sep (fun _ -> str",") pr_uconstraint v) (* Gallina extensions *) | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id) |