From 3ef2bd35926a83fbcfd34d03e1fb1db894a39627 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 8 Jul 2020 14:06:19 +0200
Subject: declare: Add [save_regular] API for obligation-ignoring proofs

---
 vernac/declare.ml  | 8 ++++++++
 vernac/declare.mli | 7 +++++++
 2 files changed, 15 insertions(+)

(limited to 'vernac')

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
 
-- 
cgit v1.2.3