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.

---
 test-suite/success/polymorphism.v | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3