HoTT/HoTT — pull request #392 by JasonGross (2014-05-13 19:29:15+00:00)
Title: No custom stdlib

Instead replace the relevant constants on top of the standard library.
This is less nice, because it allows access to the evil [eq], but it
means we can use lemmas in the standard library about things like [le]
and [nat] and [bool]. Also tactics. Also, we won't have to port and
maintain the whole standard library. Also (the real reason here) I
couldn't figure out how to get the replacement to compile with Coq
trunk, and I want to ease the (eventual) switch to trunk.

We should be able to strip out the constants from the standard library
replacement file, as they become polymorphic in trunk. (I'm still
holding out hope that the standard library [sigT] of 8.5 will be both
polymorphic and a primitive record.