diff options
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 |