Jason Gross

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

1

The code at https://github.com/JasonGross/HoTT-categories/blob/coq-bug-004/theories/NaturalTransformation/Composition/Functorial.v#L33 gives ``` Toplevel input, characters 0-323: Anomaly: Uncaught exception Not_found(_). Please report. frame @ file "toplevel/vernac.ml", line 343, characters 6-16 raise @ file "toplevel/vernac.ml", line 335,...

Anomaly: Mismatched instance and context when building universe substitution.

1

``` bash jgross@cagnode17:~/HoTT$ cat /tmp/foobug.v Inductive paths A (x : A) : A -> Type := idpath : paths A x x. Notation "x = y" := (paths _ x...

Ltac unification should either ignore universe constraints, deferring them to when the proof tree is built, or should update universe constraints

3

I want the following code to work: ``` coq Goal Type = Type. match goal with |- ?x = ?x => idtac end. ``` I'm not sure what the behavior...

Here is some code that works in 8.4 and not in trunk-polyproj: ``` coq (* File reduced by coq-bug-finder from 64 lines to 30 lines. *) Set Implicit Arguments. Set...

This code works in HoTT/coq trunk, but not trunk-polyproj (is this the inductive problem of https://github.com/HoTT/coq/issues/95#issuecomment-39706988?) ``` coq Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Record SpecializedCategory (obj...

``` coq (* File reduced by coq-bug-finder from 335 lines to 115 lines. *) Set Implicit Arguments. Set Universe Polymorphism. Generalizable All Variables. Record Category (obj : Type) := Build_Category...

``` coq (* File reduced by coq-bug-finder from 138 lines to 78 lines. *) Set Implicit Arguments. Generalizable All Variables. Set Universe Polymorphism. Delimit Scope object_scope with object. Delimit Scope...

Sometimes I get `Cannot enforce tmpJT_kQC.10643 = Set because Set

``` coq Set Implicit Arguments. Set Universe Polymorphism. Notation idmap := (fun x => x). Inductive paths {A : Type} (a : A) : A -> Type := idpath :...

The eliminators for records with eta should just be defined as function application or the identity function, not using pattern matching: ``` coq Set Implicit Arguments. Require Import Logic. Global...