diff options
| -rw-r--r-- | stm/lemmas.ml | 14 |
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 = |