Changed semantics of induction !id when a clause is given: don't
authoritatively erase non-generalized hypotheses dependent on id.
Adapting to naming of evars.
Add a boolean to indicate the unfolding state of a primitive projection,
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
Make pattern_of_constr typed so that we can infer the proper patterns
for primitive projections, fixing bug #3661. Also fix expand_projection
so that it does enough reduction to find the inductive type of its
argument.
Bug fixed.
Fix bug 3662 by actually reducing primitive projections in cbv/compute.
Fix bug #3672, application of primitive projections as coercions.
Fix semantics of matching with folded/unfolded projections to definitely
avoid looping and be compatible with unfold.
Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr.
Fix bug #3664 by refolding projections that don't reduce in cbn.
Fix test-suite file.
First version of keyed subterm selection in unification.
Index keys instead of simply global references.
Keyed unification option, compiling the whole standard library
(but deactivated still).

Set Keyed Unification to activate the option, which changes
subterm selection to _always_ use full conversion _after_ finding a
subterm whose head/key matches the key of the term we're looking for.
This applies to rewrite and higher-order unification in
apply/elim/destruct.

Most proof scripts already abide by these semantics. For those that
don't, it's usually only a matter of using:

Declare Equivalent Keys f g.

This make keyed unification consider f and g to match as keys.
This takes care of most cases of abbreviations: typically Def foo :=
bar and rewriting with a bar-headed lhs in a goal mentioning foo works
once they're set equivalent.
For canonical structures, these hints should be automatically declared.

For non-global-reference headed terms, the key is the constructor name
(Sort, Prod...). Evars and metas are no keys.

INCOMPATIBILITIES:
In FMapFullAVL, a Function definition doesn't go through with keyed
unification on.