diff options
| author | Matthieu Sozeau | 2014-07-25 11:09:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-25 11:09:01 +0200 |
| commit | 2c033252edf2102533d91a0ca7368f031008a17f (patch) | |
| tree | 34e603c800ccf3cb93dfb0f817beb66992c5e556 /proofs/proof_global.mli | |
| parent | 0ee6bd8de352e5e3129ab66186be1eee1d4ba1af (diff) | |
Fix handling of universes at the end of proofs, esp. for async proof processing.
Thanks to E. Tassi for the initial patch.
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 d8e84d0aa7..b0e53ecd87 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -95,7 +95,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 *) -type closed_proof_output = Entries.proof_output list * Evd.evar_universe_context +type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context val return_proof : unit -> closed_proof_output val close_future_proof : feedback_id:Stateid.t -> |