Merge pull request #28 from andrejbauer/ssreflect

Ssreflect
Added theorem [forall_hlevel], that h-levels are closed under arbitrary products.
Minor proof simplifications (lemmas about hprops are instances of lemmas about general h-levels).
Merge pull request #29 from peterlefanulumsdaine/pll_master

Added lemma [forall_hlevel], that h-levels are closed under arbitrary products.
Make the code work with the latest coq + univ polymorphism. Stopping
in Univalence due to a universe inconistency/unification issue, not
sure which yet.
- Change relevant_equality to parameters_matter option
- Add hoqtop.byte script
- Adapt the autoconf/automake scripts
- An undo_compose_map was diverging in Equivalences, replaced with a rewrite.
- Compile everything with the latest version of HoTT/coq

Note that univalence_implies_weak_funext requires two different
uses of the univalence axiom hence we need to have the hypothesis
twice (section variables are not polymorphic, yet).
No need for two instances of the eta_dep_rule hypothesis in Funext.v
Rename parameters_matter to indices_matter
Remove references to hoqtop.byte.in, because configure was not testing properly for existence of coqtop.byte, and hoqtop.byte.in was missing
Still some other references to hoqtop.byte
Merge pull request #31 from andrejbauer/master

Placing the new ssreflect-like version of HoTT onto the main repo.
Add some preliminary definitions of Coq.Init.Logic so that tauto does not fail with
a GlobalizationError.
Merge branch 'master' of github.com:HoTT/HoTT
arrange for one dependency file per *.v file, rather than one big one
Merge pull request #36 from DanGrayson/master

fix dependencies
Merge pull request #37 from andrejbauer/master

Improvements to the library, optional compilation of ssreflect (because it is currently broken)
New flag to set for compat with latest trunk
- Add hoqtop.byte target
- Add Set Asymmetric Patterns and Set Universe Polymorphism global flags
(shouldn't affect other versions without the flags).
- A little fix in theories/Equivalence due to a failed eta conversion
in unification (not related to universes though). Investigating this.
Merge pull request #38 from andrejbauer/master

Mike's Record tactics and a fix in hoqide
Merge branch 'ssreflect' into 'master'.

This is a major merge with which we are commencing a new version of HoTT which uses
type classes and the latest version of HoTT/coq that supports -indices-matter and
universe polymorphism.

The HoTT library is not quite finished at this point, but it compiles and now seems
to be a good moment to merge with master. We have tagged the version before this one
with no-ssreflect-and-type-classes. If you have your own development, proceed carefully
with upgrading the HoTT library. However, in the long run you will wish to conform your
library with HoTT.

Almost all conflicts were resolved in favor of the ssreflect branch, except for a couple
of changes made by Matthieu Sozeau.

Conflicts:
	.gitignore
	Makefile.am
	Makefile.in
	configure
	configure.ac
	contrib/old/Paths.v
	coq/theories/Init/Datatypes.v
	coq/theories/Init/Logic.v
	hoqc.in
	hoqide.in
	hoqtop.in
	theories/Contractible.v
	theories/Equivalences.v
	theories/Fibrations.v
	theories/HLevel.v