From 2d6de8b102ea3cd05c5d193190faf787ccb84baa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Apr 2014 17:29:26 +0200
Subject: Fix restrict_universe_context removing some universes that do appear
 in the term.

---
 test-suite/success/polymorphism.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 7c1166c4c4..1ef2713e44 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -243,7 +243,7 @@ Polymorphic Definition fun_ext (A B : Type) :=
 
 Polymorphic Class Funext A B := extensional : fun_ext A B.
 
-Section foo. 
+Section foo2. 
   Context `{forall A B, Funext A B}.
   Print Universes.
-End foo.
+End foo2.
-- 
cgit v1.2.3