diff options
| -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 = |