From 9f1f8e29baa6d8f8d458740737d0fbd02de31c6c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 24 Jun 2014 17:17:46 +0200
Subject: Force the final universe context of a proof only in poly || now case.

---
 proofs/proof_global.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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