From 848bc5b5fc366ab5869a2836c5ad83ab4d0f2842 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 May 2017 15:31:16 +0200
Subject: [vernac] Remove `Qed exporting` syntax.

We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.

Next step, understand why.
---
 printing/ppvernac.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index f371fb08c7..10dd42ea91 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -718,10 +718,7 @@ open Decl_kinds
         match o with
           | None -> (match opac with
               | Transparent -> keyword "Defined"
-              | Opaque None -> keyword "Qed"
-              | Opaque (Some l) ->
-                  keyword "Qed" ++ spc() ++ str"export" ++
-                    prlist_with_sep (fun () -> str", ") pr_lident l)
+              | Opaque      -> keyword "Qed")
           | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
       )
       | VernacExactProof c ->
-- 
cgit v1.2.3