diff options
| author | Matthieu Sozeau | 2014-06-24 17:17:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-24 18:53:52 +0200 |
| commit | 9f1f8e29baa6d8f8d458740737d0fbd02de31c6c (patch) | |
| tree | 87a7430f91e1f8add978f5529dccc1cfc8ceba77 | |
| parent | 03cab057c3ccc51464ed69531441d3c09b2919a7 (diff) | |
Force the final universe context of a proof only in poly || now case.
| -rw-r--r-- | proofs/proof_global.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 410335b47e..06afc2fa9a 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -269,7 +269,10 @@ let close_proof ?feedback_id ~now fpl = let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let fpl, univs = Future.split2 fpl in - let universes = Future.force univs in + let universes = + if poly || now then Future.force univs + else Proof.in_proof proof (fun x -> Evd.evar_universe_context x) + in let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) (Evd.evar_universe_context_subst universes) in let make_body = |