diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacextend.ml | 7 | ||||
| -rw-r--r-- | vernac/vernacextend.mli | 7 |
2 files changed, 6 insertions, 8 deletions
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 *) |