From a44b97e3e7f4a302a5255ca9fc57ea0b81a36b7e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 18 Oct 2018 13:04:32 +0200
Subject: Do not qualify universe names by section path.

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

(limited to 'test-suite')

diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v
index 1827e54d76..1bc565cbb5 100644
--- a/test-suite/success/unidecls.v
+++ b/test-suite/success/unidecls.v
@@ -46,12 +46,12 @@ Universe secfoo.
 Section Foo'.
   Fail Universe secfoo.
   Universe secfoo2.
-  Check Type@{Foo'.secfoo2}.
+  Fail Check Type@{Foo'.secfoo2}.
+  Check Type@{secfoo2}.
   Constraint secfoo2 < a.
 End Foo'.
 
 Check Type@{secfoo2}.
-Fail Check Type@{Foo'.secfoo2}.
 Fail Check eq_refl : Type@{secfoo2} = Type@{a}.
 
 (** Below, u and v are global, fixed universes *)
-- 
cgit v1.2.3