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.