diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-22 14:58:01 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:58:32 +0100 |
| commit | 671f216c27e7ca9f57976eab03c667f09b850d51 (patch) | |
| tree | 7d71312b313e55b379d9dfb44ba903c8a9af0bc6 /proofs | |
| parent | 29aa2d94b253dad0ade8c877fd7f46b8537a5847 (diff) | |
Cosmetic: add an expected newline in proof_global.
Diffstat (limited to 'proofs')
| -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) |