adding [Funext-comp-rules.v], a discussion of computation rules for functional extensionality.
Folding content of [Funext-comp-rules.v] into [Funext.v].
Removing [Funext-comp-rules.v].
Personalising readme.
Added statement of [contr_funext], and proof of it from [funext_dep].
Merge branch 'master' of github.com:peterlefanulumsdaine/HoTT
Trying to understand Ltac second-order pattern-matching
Joining the dots from naive to strong funext.
Fixing breakage in prev commit
Major reorganisation of Funext.v
Adding archive copy of blog post menagerie.html
Adding derivation(s) of dependent from non-dependent W-types.
Renaming to w-to-inductive.v to make use of builtin equality explicit.
Starting on fetooling of w-to-inductive.v without rewrite; ack, it’s painful.
Minor correction to previous commit.
Committing changes that were over a very old version of upstream, for later re-basing.
Merge pull request #59 from andrejbauer/master

Added a convenience file theories/HoTT.v which exports the rest of the librarary
Draft of a style guide.
one fix
Merge pull request #60 from mikeshulman/forupstream

Draft of a style guide