From 4a53151f846476f2fbe038a4ecb8e84256a26ba9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 14 Feb 2015 18:35:04 +0100
Subject: Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior

Of course such proofs cannot be processed asynchronously
---
 printing/ppvernac.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e9e335ec91..e0b94669c2 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -740,9 +740,14 @@ module Make
 
         | VernacEndProof (Proved (opac,o)) -> return (
           match o with
-            | None -> if opac then keyword "Qed" else keyword "Defined"
+            | 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)
             | Some (id,th) -> (match th with
-                | None -> (if opac then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
+                | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
                 | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)
         )
         | VernacExactProof c ->
-- 
cgit v1.2.3