From d7f11221f797e501fe3bcdb06fe7ef3f559869c3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 19 Aug 2019 16:46:20 +0200
Subject: Fix #10669 incorrect substitution in context outside section

---
 test-suite/output/UnivBinders.out | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite/output')

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index a89fd64999..d13ea707bb 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -157,12 +157,12 @@ Type@{UnivBinders.58} -> Type@{i}
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axbar
-axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i}
+axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo'
-axbar' : Type@{axbar'.u0} -> Type@{axbar'.i}
+axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
-- 
cgit v1.2.3