diff options
| -rw-r--r-- | proofs/proof_global.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 8b5b739a3..15f34ccc6 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -169,6 +169,7 @@ let with_current_proof f = let p = { p with proof = newpr } in pstates := p :: rest; ret + let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ()) let compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact) |