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.
Added an etags command for making a TAGS file.  See INSTALL.txt for
usage.  Next goal: provide a linear ordering for all the *.v files
so M-. and M-x tags-search find first things first.
Added a convenience file theories/HoTT.v which exports the rest of the library.

A development based on the HoTT library can now import most, if not all of it
by "Require Import HoTT".
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.