From 328dbe5eb9b2b1eec18d32c135e517394cd6efc3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 27 Dec 2014 20:38:58 +0100
Subject: 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.
---
 proofs/proof_global.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
 
-- 
cgit v1.2.3