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".