diff options
| author | Gaëtan Gilbert | 2018-11-05 13:06:06 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-23 13:53:05 +0100 |
| commit | 4cfb46eb803614ea3fbe40fe6fd26b8c1290e302 (patch) | |
| tree | 0357c6487e2d32f9913a4d92b21b6de198375130 /vernac | |
| parent | ed04b8eb07ca3925af852c30a75c553c134f7d72 (diff) | |
change vernac_qed_type to have [VtKeep of vernac_keep_as]
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 *) |