diff options
| author | Matthieu Sozeau | 2018-11-27 11:20:57 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-11-27 11:20:57 +0100 |
| commit | f6a2d21b6c2a93cb70fde235fc897fb75ea51384 (patch) | |
| tree | 8913811d7ff06686a0ec837296545cae12007f85 /vernac | |
| parent | dddb72b2f45f39f04e91aa9099bcd1064c629504 (diff) | |
| parent | c58ea20fba5a5ce54aaf62182dfd3ee8a368d529 (diff) | |
Merge PR #8850: Private universes for opaque polymorphic constants.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 8 | ||||
| -rw-r--r-- | vernac/vernacextend.ml | 5 | ||||
| -rw-r--r-- | vernac/vernacextend.mli | 6 |
3 files changed, 13 insertions, 6 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 2443c5d12a..46d7892bf6 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 35f26cab4d..2541f73582 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -12,6 +12,10 @@ open Util open Pp open CErrors +type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque + +type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop + type vernac_type = (* Start of a proof *) | VtStartProof of vernac_start @@ -33,7 +37,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..8b07be8b16 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -27,6 +27,11 @@ considered safe to delegate to a worker. *) + +type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque + +type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop + type vernac_type = (* Start of a proof *) | VtStartProof of vernac_start @@ -48,7 +53,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 = |