diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-18 20:39:08 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:23:41 +0100 |
commit | 00860c1b2209159fb2b6780004c8c8ea16b3cb3a (patch) | |
tree | 20045d21798206cf742a4bd86668da41cef6e5cf /test-suite/success/polymorphism.v | |
parent | 34d85e1e899f8a045659ccc53bfd6a1f5104130b (diff) |
In close_proof only check univ decls with the restricted context.
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. |