Search results

Multiple definition of the extension constructor name Found.

Status: Open.

#127 In HoTT/coq;

· IFEIFEI opened on Dec 29, 2020

Anomaly: variable n unbound. (using [transparent assert])

Status: Open.

#126 In HoTT/coq;

· RobertoZunino opened on Sep 30, 2015

Syntax for explicit universe levels

Status: Open.

#125 In HoTT/coq;

· JasonGross opened on May 7, 2014

Universe polymorphism breaks record eta (polyproj)

Status: Open.

#124 In HoTT/coq;

· JasonGross opened on May 2, 2014

Stack overflow on [Defined] (polyproj)

Status: Open.

#123 In HoTT/coq;

· JasonGross opened on Apr 29, 2014

Stack overflow on "Hint Rewrite @<primitive projection>" (polyproj)

Status: Open.

#122 In HoTT/coq;

· JasonGross opened on Apr 28, 2014

Error: Unsatisfied constraints: <universe constraints> (polyproj)

Status: Open.

#121 In HoTT/coq;

· JasonGross opened on Apr 27, 2014

HoTT/coq's universe inconsistencies do not respect delta (polyproj) (maybe?)

Status: Open.

#120 In HoTT/coq;

· JasonGross opened on Apr 27, 2014

Sometimes, universe polymorphic definitions aren't polymorphic enough (but making them more polymorphic might break other things) (polyproj)

Status: Open.

#119 In HoTT/coq;

· JasonGross opened on Apr 22, 2014

Error: Unable to satisfy the following constraints (bug in typeclass resolution?) (polyproj)

Status: Open.

#118 In HoTT/coq;

· JasonGross opened on Apr 21, 2014

Anomaly: not an arity. Please report. (polyproj)

Status: Open.

#115 In HoTT/coq;

· JasonGross opened on Apr 20, 2014

"Unable to handle arbitrary u+k <= v constraints" should probably be an Error, not an Anomaly (polyproj)

Status: Open.

#114 In HoTT/coq;

· JasonGross opened on Apr 20, 2014