From 671f216c27e7ca9f57976eab03c667f09b850d51 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 22 Feb 2018 14:58:01 +0100 Subject: Cosmetic: add an expected newline in proof_global. --- proofs/proof_global.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'proofs') 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) -- cgit v1.2.3