diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/namedunivs.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |