diff options
| author | Enrico Tassi | 2014-12-27 20:38:58 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-27 20:38:58 +0100 |
| commit | 328dbe5eb9b2b1eec18d32c135e517394cd6efc3 (patch) | |
| tree | dea229ff4172f27323712a899ab5502c76fa5894 | |
| parent | f34946ecfb0ea2c75337369f3e41e9562be0d84b (diff) | |
proof_global: make it possible to call close_proof in a worker
Given that the proof state contains a callback (a terminator)
that is not sent (dropped by the ephemeron mechanism at marshall
time) de-referencing the ephemeron during this function makes it
impossible to call it in a worker. Now the worker can call the
function and replace the terminator with a good one.
| -rw-r--r-- | proofs/proof_global.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index d94bc86cd7..dd0e146497 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -333,7 +333,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = const_entry_polymorphic = poly}) fpl initial_goals in { id = pid; entries = entries; persistence = strength; universes = universes }, - Ephemeron.get terminator + fun pr_ending -> Ephemeron.get terminator pr_ending type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context |