diff options
Diffstat (limited to 'test-suite/success/polymorphism.v')
-rw-r--r-- | test-suite/success/polymorphism.v | 14 |
1 files changed, 13 insertions, 1 deletions
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. |