diff options
| author | Gaëtan Gilbert | 2018-10-29 17:56:10 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-23 13:53:05 +0100 |
| commit | ed04b8eb07ca3925af852c30a75c553c134f7d72 (patch) | |
| tree | 3e096da8b235708bf7e5d82e508e9319fcc413c7 /vernac/vernacextend.ml | |
| parent | 371efb58fd9b528743a79b07998a5287fbc385d2 (diff) | |
Local universes for opaque polymorphic constants.
Diffstat (limited to 'vernac/vernacextend.ml')
| -rw-r--r-- | vernac/vernacextend.ml | 6 |
1 files changed, 5 insertions, 1 deletions
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 = |