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.
---
 stm/stm.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index e0064df9bb..75ec946f03 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1385,7 +1385,7 @@ end = struct (* {{{ *)
           stm_vernac_interp stop
             ~proof:(pobject, terminator)
             { verbose = false; loc; indentation = 0; strlen = 0;
-              expr = (VernacEndProof (Proved (Opaque None,None))) }) in
+              expr = (VernacEndProof (Proved (Opaque,None))) }) in
         ignore(Future.join checked_proof);
       end;
       RespBuiltProof(proof,time)
@@ -1525,7 +1525,7 @@ end = struct (* {{{ *)
       Reach.known_state ~cache:`No start;
       stm_vernac_interp stop ~proof
         { verbose = false; loc; indentation = 0; strlen = 0;
-          expr = (VernacEndProof (Proved (Opaque None,None))) };
+          expr = (VernacEndProof (Proved (Opaque,None))) };
       `OK proof
       end
     with e ->
@@ -1976,7 +1976,6 @@ let collect_proof keep cur hd brkind id =
    | id :: _ -> Names.Id.to_string id in
  let loc = (snd cur).loc in
  let rec is_defined_expr = function
-   | VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) -> true
    | VernacTime (_, e) -> is_defined_expr e
    | VernacRedirect (_, (_, e)) -> is_defined_expr e
    | VernacTimeout (_, e) -> is_defined_expr e
-- 
cgit v1.2.3