From ed04b8eb07ca3925af852c30a75c553c134f7d72 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 29 Oct 2018 17:56:10 +0100
Subject: Local universes for opaque polymorphic constants.

---
 vernac/lemmas.ml        | 8 ++++----
 vernac/vernacextend.ml  | 6 +++++-
 vernac/vernacextend.mli | 7 ++++++-
 3 files changed, 15 insertions(+), 6 deletions(-)

(limited to 'vernac')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index de020926f6..5204a16f9c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -311,7 +311,7 @@ let universe_proof_terminator compute_guard hook =
       | Transparent -> false, true
       | Opaque      -> true, false
     in
-    let const = {const with const_entry_opaque = is_opaque} in
+    assert (is_opaque == const.const_entry_opaque);
     let id = match idopt with
       | None -> id
       | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
@@ -498,13 +498,13 @@ let save_proof ?proof = function
             Admitted(id,k,(sec_vars, (typ, ctx), None), universes)
       in
       Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
-  | Vernacexpr.Proved (is_opaque,idopt) ->
+  | Vernacexpr.Proved (opaque,idopt) ->
       let (proof_obj,terminator) =
         match proof with
         | None ->
-            Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)
+            Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)
         | Some proof -> proof
       in
       (* if the proof is given explicitly, nothing has to be deleted *)
       if Option.is_empty proof then Proof_global.discard_current ();
-      Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
+      Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj)))
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 3a321ecdb4..23e1223501 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -12,6 +12,11 @@ open Util
 open Pp
 open CErrors
 
+type vernac_qed_type =
+  | VtKeep of Proof_global.opacity_flag
+  | VtKeepAsAxiom
+  | VtDrop
+
 type vernac_type =
   (* Start of a proof *)
   | VtStartProof of vernac_start
@@ -33,7 +38,6 @@ type vernac_type =
   (* To be removed *)
   | VtMeta
   | VtUnknown
-and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
 and vernac_start = string * opacity_guarantee * Names.Id.t list
 and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 7feaccd9a3..07ba6ee00d 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -27,6 +27,12 @@
    considered safe to delegate to a worker.
 
 *)
+
+type vernac_qed_type =
+  | VtKeep of Proof_global.opacity_flag (** Defined/Qed *)
+  | VtKeepAsAxiom (** Admitted *)
+  | VtDrop (** Abort *)
+
 type vernac_type =
   (* Start of a proof *)
   | VtStartProof of vernac_start
@@ -48,7 +54,6 @@ type vernac_type =
   (* To be removed *)
   | VtMeta
   | VtUnknown
-and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
 and vernac_start = string * opacity_guarantee * Names.Id.t list
 and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =
-- 
cgit v1.2.3


From 4cfb46eb803614ea3fbe40fe6fd26b8c1290e302 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 5 Nov 2018 13:06:06 +0100
Subject: change vernac_qed_type to have [VtKeep of vernac_keep_as]

---
 vernac/vernacextend.ml  | 7 +++----
 vernac/vernacextend.mli | 7 +++----
 2 files changed, 6 insertions(+), 8 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 23e1223501..5bea257875 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -12,10 +12,9 @@ open Util
 open Pp
 open CErrors
 
-type vernac_qed_type =
-  | VtKeep of Proof_global.opacity_flag
-  | VtKeepAsAxiom
-  | VtDrop
+type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque
+
+type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop
 
 type vernac_type =
   (* Start of a proof *)
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 07ba6ee00d..8b07be8b16 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -28,10 +28,9 @@
 
 *)
 
-type vernac_qed_type =
-  | VtKeep of Proof_global.opacity_flag (** Defined/Qed *)
-  | VtKeepAsAxiom (** Admitted *)
-  | VtDrop (** Abort *)
+type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque
+
+type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop
 
 type vernac_type =
   (* Start of a proof *)
-- 
cgit v1.2.3