In close_proof only check univ decls with the restricted context.

2 files changed, 15 insertions, 2 deletions

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
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 930c165178..c09a60a4d7 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -405,13 +405,25 @@ Module Restrict.
   (* Universes which don't appear in the term should be pruned, unless they have names *)
   Set Universe Polymorphism.
 
-  Definition dummy_pruned@{} : nat := ltac:(let x := constr:(Type) in exact 0).
+  Ltac exact0 := let x := constr:(Type) in exact 0.
+  Definition dummy_pruned@{} : nat := ltac:(exact0).
 
   Definition named_not_pruned@{u} : nat := 0.
   Check named_not_pruned@{_}.
 
   Definition named_not_pruned_nonstrict : nat := ltac:(let x := constr:(Type@{u}) in exact 0).
   Check named_not_pruned_nonstrict@{_}.
+
+  Lemma lemma_restrict_poly@{} : nat.
+  Proof. exact0. Defined.
+
+  Unset Universe Polymorphism.
+  Lemma lemma_restrict_mono_qed@{} : nat.
+  Proof. exact0. Qed.
+
+  Lemma lemma_restrict_abstract@{} : nat.
+  Proof. abstract exact0. Qed.
+
 End Restrict.
 
 Module F.