- Fix index-list to show computational relations for rewriting files.
- Fix hasheq which didn't have a case for Proj making hashconsing exponentially slower.
Cleanup in constr, correct classification of polymorphic defs.
- Fix handling of polymorphic inductive elimination schemes.
- Avoid generation of dummy universes for unsafe_global*
- Handle side effects better for polymorphic definitions.
- Fix abstract forgetting about new constraints.
Adapt Y. Bertot's path on private inductives (now the keyword is "Private").

A quick and dirty approach to private inductive types
Types for which computable functions are provided, but pattern-matching is disallowed.
This kind of type can be used to simulate simple forms of higher inductive types, with
convertibility for applications of the inductive principle to 0-constructors

Conflicts:
	intf/vernacexpr.mli
	kernel/declarations.ml
	kernel/declarations.mli
	kernel/entries.mli
	kernel/indtypes.ml
	library/declare.ml
	parsing/g_vernac.ml4
	plugins/funind/glob_term_to_relation.ml
	pretyping/indrec.ml
	pretyping/tacred.mli
	printing/ppvernac.ml
	toplevel/vernacentries.ml
MSWin Fixes

Conflicts:
	configure