diff options
| author | Hugo Herbelin | 2017-04-02 11:21:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-09 11:52:17 +0200 |
| commit | 1a43fda0dc9bb8d100808426980446353f8f1ae3 (patch) | |
| tree | 5907412903414e3c21d718a70dc0d377a3589b1a /printing | |
| parent | 2c0287fe8445bd4b599bf8498bcb71b2a7df0d51 (diff) | |
Removing internal support for accepting "{struct x}" and co in "Theorem with".
There were actually no syntax for it, and I'm still unsure what good
syntax to give to it, even more that it would be useful to have one.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index cfc2e48d11..d3b4007fbe 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -386,13 +386,12 @@ open Decl_kinds ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def ++ prlist (pr_decl_notation pr_constr) ntn - let pr_statement head (idpl,(bl,c,guard)) = + let pr_statement head (idpl,(bl,c)) = assert (not (Option.is_empty idpl)); let id, pl = Option.get idpl in hov 2 (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ - pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++ str":" ++ pr_spc_lconstr c) let pr_priority = function |