From be030aef23a094aff85de6066cb97d5c110d56ae Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 26 Dec 2013 11:22:12 +0100
Subject: Lemmas: export standard proof terminator

---
 stm/lemmas.ml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

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