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 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'printing/ppvernac.ml')

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


From 74826c1869a423b4e7224d3f69180584bdef1726 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 27 Sep 2017 16:54:41 +0200
Subject: Parse [Proof using Type] without translating Type to an id.

---
 printing/ppvernac.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'printing/ppvernac.ml')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 4c68285f3f..d1158b3d6f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -527,6 +527,7 @@ open Decl_kinds
   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^")"
-- 
cgit v1.2.3