diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 11 | ||||
| -rw-r--r-- | printing/ppvernac.mli | 3 |
2 files changed, 13 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a1cdfdbaa2..d1158b3d6f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -524,7 +524,16 @@ 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 -> "()" + | SsType -> "(Type)" + | 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 |