Some Coq patches
A patch against Coq 8.3, 8.3pl1 or 8.3pl2 that provides
η-conversion [github].
A patch against Coq 8.3, 8.3pl1,
8.3pl2 (but also 8.2 and trunk) that removes universe consistency
checks (and incidentally makes Coq inconsistent).
I had
a patch
enforcing constraints on inductive types in Set and Type so that it
complies with the homotopy approach (in the sense that the typing of
inductive types with indices comply with an interpretation of the
inductive types where indices such as (a:A) are interpreted as
equality (a=a:A) added to the set of arguments of the constructors,
and these equalities themselves interpreted as a unit or empty type
when over elements in A:Prop or A:Set and virtually as morphisms when
over elements in A:Type).
This patch first did not address the issue of singleton elimination
and secondly put a slightly stronger restriction than needed on the
typing of inductive types in Type. I plan to come back to this by the
end of May.
Patches have to be applied in the Coq source directory using "patch -p1 < name-of-patch".