Jason Gross

Alternatively (to passing `-coqlib`), I can just `Set Universe Polymorphism`. This is still open in trunk-polyproj.

Here's a slightly simpler example: ``` coq Set Universe Polymorphism. Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x. Notation...

What I was most worried about was inferring inconsistent constraints in two different instances of typeclass resolution, when if the instances had happened together, there would have been no such...

Fixed in trunk-polyproj (but not in HoTT/coq trunk), so I think we (@jcmckeown or @mattam82) should close this bug.

Here is code that used to be accepted, but is no longer, which hopefully explicates the problem. I think it is valid (and useful); do I think incorrectly? (It seems...

I suspect the dependence on the stdlib was actually a dependence on `Set Universe Polymorphism.`

Here is one way to implement this rule: add half-eta-expansion for all inductive types which refreshes universes in the return type to the conversion machinery, and trigger this on universe...

If you can make this go through at pretyping time, then I think you're good: ``` coq Inductive paths {A : Type} (a : A) : A -> Type :=...

I have not tried that branch. I just tried to compile it, and got ``` $ ./configure -debug -prefix "$(readlink -f ~/.local64)" ... $ make -j16 -k ... $ make...

I have tried removing the arguments to `./configure`; I still get a segfault. Is is possible that my version of ocaml 4.00.1 is too new or something?