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.
---
 intf/vernacexpr.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index cfc3343b61..03e8ea43d1 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -139,8 +139,7 @@ type search_restriction =
 
 type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
-                           (*   list of idents for qed exporting           *)
-type opacity_flag   = Opaque of lident list option | Transparent
+type opacity_flag   = Opaque | Transparent
 type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
   (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
-- 
cgit v1.2.3