Issues

• Multiple definition of the extension constructor name Found.

  HoTT/coq#127 · Filter by author IFEIFEI opened on Dec 29, 2020
  1

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

  HoTT/coq#126 · Filter by author RobertoZunino opened on Sep 30, 2015

• Syntax for explicit universe levels

  HoTT/coq#125 · Filter by author JasonGross opened on May 7, 2014
  2

• Universe polymorphism breaks record eta (polyproj)

  HoTT/coq#124 · Filter by author JasonGross opened on May 2, 2014

• Stack overflow on [Defined] (polyproj)

  HoTT/coq#123 · Filter by author JasonGross opened on Apr 29, 2014

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

  HoTT/coq#122 · Filter by author JasonGross opened on Apr 28, 2014

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

  HoTT/coq#121 · Filter by author JasonGross opened on Apr 27, 2014

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

  HoTT/coq#120 · Filter by author JasonGross opened on Apr 27, 2014
  13

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

  HoTT/coq#119 · Filter by author JasonGross opened on Apr 22, 2014

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

  HoTT/coq#118 · Filter by author JasonGross opened on Apr 21, 2014

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

  HoTT/coq#115 · Filter by author JasonGross opened on Apr 20, 2014

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

  HoTT/coq#114 · Filter by author JasonGross opened on Apr 20, 2014

• [change ... in *] picks universes once, which unifies universes too eagerly (polyproj)

  HoTT/coq#113 · Filter by author JasonGross opened on Apr 20, 2014

• Application Error: The 1st term has type "Univalence (* Top.934 Top.935 Top.936 Top.937 *)" which should be coercible to "Univalence (* Top.1003 Top.1003 Top.1001 Top.997 *)". (polyproj)

  HoTT/coq#112 · Filter by author JasonGross opened on Apr 15, 2014

• [abstract] duplicates fresh lemmas in universe polymorphic mode (polyproj)

  HoTT/coq#111 · Filter by author JasonGross opened on Apr 15, 2014
  1

• Anomaly: Uncaught exception Not_found(_). Please report. (polyproj)

  HoTT/coq#110 · Filter by author JasonGross opened on Apr 15, 2014

• abstract creates duplicate theorems / Anomaly: Backtrack.backto 55: a state with no vcs_backup. Please report. (polyproj)

  HoTT/coq#108 · Filter by author JasonGross opened on Apr 15, 2014

• Universe inconsistency where there didn't used to be one (polyproj) (Set vs Type)

  HoTT/coq#107 · Filter by author JasonGross opened on Apr 15, 2014

• "Error: Unable to satisfy the following constraints:" on typeclass inference (polyproj) (Also, error message is missing some newlines)

  HoTT/coq#106 · Filter by author JasonGross opened on Apr 14, 2014
  5

• Primitive projections break some argument inference (polyproj)

  HoTT/coq#105 · Filter by author JasonGross opened on Apr 8, 2014

• not convertible error where there didn't used to be one (polyproj)

  HoTT/coq#102 · Filter by author JasonGross opened on Apr 8, 2014

• Universe inconsistency where there didn't used to be one (polyproj)

  HoTT/coq#101 · Filter by author JasonGross opened on Apr 8, 2014

• Universe inconsistency where there didn't used to be one (Set vs Type) (polyproj)

  HoTT/coq#100 · Filter by author JasonGross opened on Apr 8, 2014

• Error: Unsatisfied constraints on Variable (polyproj)

  HoTT/coq#99 · Filter by author JasonGross opened on Apr 8, 2014

• Universe inconsistencies depend oddly on the stdlib (polyproj)

  HoTT/coq#93 · Filter by author JasonGross opened on Mar 23, 2014
  6