From 848bc5b5fc366ab5869a2836c5ad83ab4d0f2842 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
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.
---
 API/API.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 654d93485..ea4a1ceb2 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3670,7 +3670,7 @@ sig
   type lname = Names.Name.t Loc.located
   type lident = Names.Id.t Loc.located
   type opacity_flag =
-                    | Opaque of lident list option
+                    | Opaque
                     | Transparent
   type locality_flag = bool
   type inductive_kind =
-- 
cgit v1.2.3