From 7f1635816588ae200c8eed381d726bd29f57d899 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 27 Sep 2017 16:12:58 +0200
Subject: [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.
---
 printing/ppvernac.ml  | 10 +++++++++-
 printing/ppvernac.mli |  3 +++
 2 files changed, 12 insertions(+), 1 deletion(-)

(limited to 'printing')

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
-- 
cgit v1.2.3