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