Jason Gross
Jason Gross
``` coq (* -*- mode: coq; coq-prog-args ("-emacs" "-indices-matter") -*- *) (* NOTE: This bug is only triggered with -load-vernac-source / in interactive mode. *) (* File reduced by coq-bug-finder...
``` coq (* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260...
``` coq (* File reduced by coq-bug-finder from original input, then from 5631 lines to 557 lines, then from 526 lines to 181 lines, then from 189 lines to 154...
``` coq Inductive test : $(let U := type of Type in exact U)$ := t. (* Anomaly: Unable to handle arbitrary u+k
``` coq Inductive T : let U := Type in U := t. (* Anomaly: not an arity. Please report. *) ``` This works in trunk, but not in trunk-polyproj.
Here is some code that works in 8.4pl3 and HoTT/coq, but fails in trunk-polyproj ``` coq (* File reduced by coq-bug-finder from original input, then from 3329 lines to 153...
``` coq (* -*- mode: coq; coq-prog-args: ("-nois" "-emacs") -*- *) (* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then...
``` coq (* File reduced by coq-bug-finder from 4464 lines to 4137 lines, then from 3683 lines to 118 lines, then from 124 lines to 75 lines. \ *) Set...
``` coq Set Universe Polymorphism. Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x. Notation "x = y" := (@paths...
``` coq Inductive paths A (x : A) : A -> Type := idpath : paths A x x. Notation "x = y" := (@paths _ x y) : type_scope....