diff options
| author | Matthieu Sozeau | 2014-08-18 18:45:22 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-18 18:45:22 +0200 |
| commit | 4684ae383a6ee56b4717026479eceb3b41b45ab0 (patch) | |
| tree | 1a17de891bdbe8a25b02c358a8c2af0267b6a1f5 | |
| parent | c54b186ecef5c71604b9b57acef278a0d09a4096 (diff) | |
Fix test-suite file.
| -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 5c0a3c7f23..967e13bbc5 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. |