diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:27:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:27:09 +0200 |
| commit | 0413899668e8be15df5065abdaf1d40ad3c2c31b (patch) | |
| tree | 5d2c4671737b9d0c9eba68cdf0d16503c6e47608 /test-suite/success/namedunivs.v | |
| parent | d7db69dea59cddd3ac81ed469170fad889af4e16 (diff) | |
Fix checker to handle projections with eta and universe polymorphism correctly.
Diffstat (limited to 'test-suite/success/namedunivs.v')
| -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 967e13bbc..5c0a3c7f2 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. |