as requested, anomaly please report about coq HOT 4 CLOSED

This does not happen anymore in the latest version (with a Universe Polymorphic HoTT/ssreflect branch).

from coq.

OK, that's good. Now, can you explain what/why, after processing to the end of the current Test.v, the Check responds

The term "@equiv_path_universe (* Top.11 Top.12 Top.13 Top.14 Top.268 *) H X Y"
has type
 "Equiv (* Top.266 Top.267 *) (Equiv (* Top.266 Top.266 *) X Y)
    (@paths (* Top.267 *) Type (* Top.266 *) X Y)"
 while it is expected to have type
 "Equiv (* Top.13 Top.13 *) (Equiv (* Top.261 Top.262 *) X Y)
    (@paths (* Top.263 *) Type (* Top.256 *) X Y)".

I can't tell if this is a bug or what's supposed to happen (though, if it is, it's annoying), and if it's a bug whether it's different from Jason's concerns or what.

from coq.

@jcmckeown, do you still have the code that made this? I'm making a regression suite for HoTT/coq.

from coq.

Even if I did, I wouldn't know how to find it; sorry.
#MustWriteAThesis

from coq.