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.
---
 vernac/lemmas.ml        | 17 +++++------------
 vernac/obligations.ml   |  6 +++---
 vernac/vernacentries.ml |  2 +-
 3 files changed, 9 insertions(+), 16 deletions(-)

(limited to 'vernac')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 4b36c2d07..192dd027c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -309,12 +309,6 @@ let get_proof proof do_guard hook opacity =
   in
   id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
 
-let check_exist =
-  List.iter (fun (loc,id) ->
-    if not (Nametab.exists_cci (Lib.make_path id)) then
-        user_err ?loc  (pr_id id ++ str " does not exist.")
-  )
-
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in
   make_terminator begin function
@@ -322,17 +316,16 @@ let universe_proof_terminator compute_guard hook =
       admit (id,k,pe) pl (hook (Some ctx)) ();
       Feedback.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
-      let is_opaque, export_seff, exports = match opaque with
-        | Vernacexpr.Transparent -> false, true, []
-        | Vernacexpr.Opaque None -> true, false, []
-        | Vernacexpr.Opaque (Some l) -> true, true, l in
+      let is_opaque, export_seff = match opaque with
+        | Vernacexpr.Transparent -> false, true
+        | Vernacexpr.Opaque      -> true, false
+      in
       let proof = get_proof proof compute_guard
 	(hook (Some (fst proof.Proof_global.universes))) is_opaque in
       begin match idopt with
       | None -> save_named ~export_seff proof
       | Some (_,id) -> save_anonymous ~export_seff proof id
-      end;
-      check_exist exports
+      end
   end
 
 let standard_proof_terminator compute_guard hook =
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 89b18d254..81218308f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -846,9 +846,9 @@ let obligation_terminator name num guard hook auto pf =
       let obl = obls.(num) in
       let status =
         match obl.obl_status, opq with
-        | (_, Evar_kinds.Expand), Vernacexpr.Opaque _ -> err_not_transp ()
-        | (true, _), Vernacexpr.Opaque _ -> err_not_transp ()
-        | (false, _), Vernacexpr.Opaque _ -> Evar_kinds.Define true
+        | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp ()
+        | (true, _), Vernacexpr.Opaque -> err_not_transp ()
+        | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true
         | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false
         | (_, status), Vernacexpr.Transparent -> status
       in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ee84ff101..ccae4359e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -507,7 +507,7 @@ let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
   let status = Pfedit.by (Tactics.exact_proof c) in
-  save_proof (Vernacexpr.(Proved(Opaque None,None)));
+  save_proof (Vernacexpr.(Proved(Opaque,None)));
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption locality poly (local, kind) l nl =
-- 
cgit v1.2.3