From 00860c1b2209159fb2b6780004c8c8ea16b3cb3a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 18 Sep 2017 20:39:08 +0200
Subject: In close_proof only check univ decls with the restricted context.

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

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index bfd64e21b0..cf5dc95fe9 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -330,7 +330,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   in
   let fpl, univs = Future.split2 fpl in
   let universes = if poly || now then Future.force univs else initial_euctx in
-  let univctx = UState.check_univ_decl ~poly universes universe_decl in
   let binders = if poly then Some (UState.universe_binders universes) else None in
   (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
@@ -375,6 +374,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
        fun t p -> Future.split2 (Future.chain p (make_body t))
     else
       fun t p ->
+        (* Already checked the univ_decl for the type universes when starting the proof. *)
+        let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in
         Future.from_val (univctx, nf t),
         Future.chain p (fun (pt,eff) ->
           (* Deferred proof, we already checked the universe declaration with
-- 
cgit v1.2.3