diff options
| author | Gaëtan Gilbert | 2020-07-08 14:06:19 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-08 15:12:46 +0200 |
| commit | 3ef2bd35926a83fbcfd34d03e1fb1db894a39627 (patch) | |
| tree | 5f7bfcaa3f191defa918ff4bcf4e07e1d280f740 /vernac | |
| parent | 22e2ab01dd9fe4d6b6afb6d1bb171cbf11db4a3f (diff) | |
declare: Add [save_regular] API for obligation-ignoring proofs
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/declare.ml | 8 | ||||
| -rw-r--r-- | vernac/declare.mli | 7 |
2 files changed, 15 insertions, 0 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index e19eca9a1c..df75e121d8 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -2068,6 +2068,14 @@ let save ~pm ~proof ~opaque ~idopt = let proof_info = process_idopt_for_save ~idopt proof.pinfo in finalize_proof ~pm proof_obj proof_info +let save_regular ~proof ~opaque ~idopt = + let open Proof_ending in + match CEphemeron.default proof.pinfo.Proof_info.proof_ending Regular with + | Regular -> + let (_, grs) : Obls_.State.t * _ = save ~pm:Obls_.State.empty ~proof ~opaque ~idopt in + grs + | _ -> CErrors.anomaly Pp.(str "save_regular: unexpected proof ending") + (***********************************************************************) (* Special case to close a lemma without forcing a proof *) (***********************************************************************) diff --git a/vernac/declare.mli b/vernac/declare.mli index d302f68153..adb5bd026f 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -214,6 +214,13 @@ module Proof : sig -> idopt:Names.lident option -> OblState.t * GlobRef.t list + (** For proofs known to have [Regular] ending, no need to touch program state. *) + val save_regular + : proof:t + -> opaque:Vernacexpr.opacity_flag + -> idopt:Names.lident option + -> GlobRef.t list + (** Admit a proof *) val save_admitted : pm:OblState.t -> proof:t -> OblState.t |