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 | |
| parent | 371efb58fd9b528743a79b07998a5287fbc385d2 (diff) | |
Local universes for opaque polymorphic constants.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 8 | ||||
| -rw-r--r-- | vernac/vernacextend.ml | 6 | ||||
| -rw-r--r-- | vernac/vernacextend.mli | 7 |
3 files changed, 15 insertions, 6 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index de020926f6..5204a16f9c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -311,7 +311,7 @@ let universe_proof_terminator compute_guard hook = | Transparent -> false, true | Opaque -> true, false in - let const = {const with const_entry_opaque = is_opaque} in + assert (is_opaque == const.const_entry_opaque); let id = match idopt with | None -> id | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in @@ -498,13 +498,13 @@ let save_proof ?proof = function Admitted(id,k,(sec_vars, (typ, ctx), None), universes) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe - | Vernacexpr.Proved (is_opaque,idopt) -> + | Vernacexpr.Proved (opaque,idopt) -> let (proof_obj,terminator) = match proof with | None -> - Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x) + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) | Some proof -> proof in (* if the proof is given explicitly, nothing has to be deleted *) if Option.is_empty proof then Proof_global.discard_current (); - Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) + Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj))) 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 = 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 = |