diff options
| author | Emilio Jesus Gallego Arias | 2017-09-27 16:12:58 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-10-10 23:50:25 +0200 |
| commit | 7f1635816588ae200c8eed381d726bd29f57d899 (patch) | |
| tree | 305b8576ee8387385b80ef4ca07491739490aa38 /printing | |
| parent | ffc91e6fcc7a1f3d719b7ad95dbbd3293e26c653 (diff) | |
[vernac] Remove "Proof using" hacks from parser.
We place `Proof_using` in the proper place [`vernac`] and we remove
gross parsing hacks.
The new placement should allow to use the printers and more convenient
structure, and reduce strange coupling between parsing and internal
representation.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 10 | ||||
| -rw-r--r-- | printing/ppvernac.mli | 3 |
2 files changed, 12 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a1cdfdbaa2..4c68285f3f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -524,7 +524,15 @@ open Decl_kinds | PrintStrategy (Some qid) -> keyword "Print Strategy" ++ pr_smart_global qid - let pr_using e = str (Proof_using.to_string e) + let pr_using e = + let rec aux = function + | SsEmpty -> "()" + | SsSingl (_,id) -> "("^Id.to_string id^")" + | SsCompl e -> "-" ^ aux e^"" + | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")" + | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")" + | SsFwdClose e -> "("^aux e^")*" + in Pp.str (aux e) let rec pr_vernac_body v = let return = tag_vernac v in diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index b88eed4843..cf27b413c0 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -15,5 +15,8 @@ val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation lis (** Prints a vernac expression *) val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.t +(** Prints a "proof using X" clause. *) +val pr_using : Vernacexpr.section_subset_expr -> Pp.t + (** Prints a vernac expression and closes it with a dot. *) val pr_vernac : Vernacexpr.vernac_expr -> Pp.t |