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.mli | |
| parent | 371efb58fd9b528743a79b07998a5287fbc385d2 (diff) | |
Local universes for opaque polymorphic constants.
Diffstat (limited to 'vernac/vernacextend.mli')
| -rw-r--r-- | vernac/vernacextend.mli | 7 |
1 files changed, 6 insertions, 1 deletions
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 = |