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.
file .depend is not optional; make it twice (it seems to help)

(this is an experiment to fix a mysterious failing build)
... same mod to one more file ... (why do I have to run autoreconf manually?)
removed detour in path construction
Merge pull request #25 from benediktahrens/small_fix_in_proof

removed detour in path construction
Merged with DanGrayson to fix .depend