Lemmas: export standard proof terminator

1 files changed, 14 insertions, 0 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 9e7bcc8b06..4f9bc8c444 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -316,6 +316,20 @@ let standard_proof_terminator compute_guard hook =
           save_anonymous_with_strength proof kind id
       end
 
+let standard_proof_terminator compute_guard hook =
+  let open Proof_global in function
+  | Admitted ->
+      admit hook ();
+      Pp.feedback Interface.AddedAxiom
+  | Proved (is_opaque,idopt,proof) ->
+      let proof = get_proof proof compute_guard hook is_opaque in
+      begin match idopt with
+      | None -> save_named proof
+      | Some ((_,id),None) -> save_anonymous proof id
+      | Some ((_,id),Some kind) -> 
+          save_anonymous_with_strength proof kind id
+      end
+
 let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = standard_proof_terminator compute_guard hook in
   let sign =