diff options
| -rw-r--r-- | proofs/proof_global.ml | 3 | ||||
| -rw-r--r-- | test-suite/success/polymorphism.v | 14 |
2 files changed, 15 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index bfd64e21b..cf5dc95fe 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 930c16517..c09a60a4d 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. |