From 4684ae383a6ee56b4717026479eceb3b41b45ab0 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 18 Aug 2014 18:45:22 +0200 Subject: Fix test-suite file. --- test-suite/success/namedunivs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/success') diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v index 5c0a3c7f2..967e13bbc 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@{j i} A) x y -> paths x y. + @paths (liftlt@{i j} A) x y -> paths x y. Proof. intros. destruct X. exact (idpath _). Defined. -- cgit v1.2.3