diff options
Diffstat (limited to 'proofs/proof_global.mli')
| -rw-r--r-- | proofs/proof_global.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index a8f2f2720..0519ac92b 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -96,7 +96,7 @@ val close_proof : (exn -> exn) -> closed_proof * Both access the current proof state. The formes is supposed to be * chained with a computation that completed the proof *) val return_proof : unit -> Entries.proof_output list -val close_future_proof : +val close_future_proof : feedback_id:Stateid.t -> Entries.proof_output list Future.computation -> closed_proof (** Gets the current terminator without checking that the proof has |