diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-07-25 11:09:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-07-25 11:09:01 +0200 |
| commit | 2c033252edf2102533d91a0ca7368f031008a17f (patch) | |
| tree | 34e603c800ccf3cb93dfb0f817beb66992c5e556 | |
| 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.
| -rw-r--r-- | proofs/proof_global.ml | 14 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 2 |
2 files changed, 9 insertions, 7 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index bfbe3dd9e..f8c7d230f 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -283,7 +283,7 @@ let close_proof ?feedback_id ~now fpl = (Evd.evar_universe_context_subst universes) in let make_body = if poly || now then - let make_body t ((c, _ctx), eff) = + let make_body t (c, eff) = let body = c and typ = nf t in let used_univs = Univ.LSet.union (Universes.universes_of_constr body) @@ -298,9 +298,11 @@ let close_proof ?feedback_id ~now fpl = fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t)) else - let univs = Evd.evar_context_universe_context universes in - fun t p -> - Future.from_val (univs, nf t), p + fun t p -> + let initunivs = Evd.evar_context_universe_context universes in + Future.from_val (initunivs, nf t), + Future.chain ~pure:true p (fun (pt,eff) -> + (pt, Evd.evar_universe_context_set (Future.force univs)), eff) in let entries = Future.map2 (fun p (_, t) -> @@ -320,7 +322,7 @@ let close_proof ?feedback_id ~now fpl = { id = pid; entries = entries; persistence = strength; universes = universes }, Ephemeron.get terminator -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 let return_proof () = let { proof } = cur_pstate () in @@ -343,7 +345,7 @@ let return_proof () = side-effects... This may explain why one need to uniquize side-effects thereafter... *) let proofs = - List.map (fun (c, _) -> ((Evarutil.nf_evars_universes evd c, Univ.ContextSet.empty), eff)) initial_goals in + List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd c, eff)) initial_goals in proofs, Evd.evar_universe_context evd let close_future_proof ~feedback_id proof = diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index d8e84d0aa..b0e53ecd8 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 -> |