From 0413899668e8be15df5065abdaf1d40ad3c2c31b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 6 Sep 2014 11:27:09 +0200
Subject: Fix checker to handle projections with eta and universe polymorphism
 correctly.

---
 test-suite/success/namedunivs.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v
index 967e13bbc5..5c0a3c7f23 100644
--- a/test-suite/success/namedunivs.v
+++ b/test-suite/success/namedunivs.v
@@ -79,7 +79,7 @@ Proof.
 Defined.
 
 Definition paths_downward_closed_lt (A : Type@{i}) (x y : A) :
-  @paths (liftlt@{i j} A) x y -> paths x y.
+  @paths (liftlt@{j i} A) x y -> paths x y.
 Proof. 
   intros. destruct X. exact (idpath _).
 Defined.
-- 
cgit v1.2.3