Fix bug #3698: stack overflow due to eta+canonical structures in
unification.
Oops, forgot a fix needed after the rebase.
Revert "Move eta-expansion after delta reduction in kernel reduction. This makes"
This makes CatsInZFC explode by expanding constants unnecessarily.
This reverts commit cf36105854c9a42960ee4139c6afdaa75ec8f31a.
Fix ML paths (thanks Jean-Marc Notin for bisecting it)
Fix -async-proofs-always-delegate (close 3740)
Add an option to not print primitive projection parameters, which can
make printing exponentially slower. We would have to expand all projections
at once before detyping to make this linear.
Implement a different strategy to expand primitive projections only when
required, i.e. in first-order unification cases where the head of the
other side is a hole or the eta-expanded constant.
Modify the heuristic for unfolding lhs or rhs in evarconv, considering
folded primitive projections in applicative stacks in rhs as named, hence
prefering to unfold the lhs in these cases.
Fix test-suite file after moving back to using C as the name
of the record binder for Class C's projections.
Reenable FO unification of primitive projections and their eta-expanded
forms in evarconv and unification, as well as fallback to first-order
unification when eta for constructors fail. Update test-suite file
3484 to test for the FO case in evarconv as well.
Fix bug 3637.
Fix test-suite files which failed due to usage of $(admit)$ which
now fails with Error: Already an existential evar of name Main
Bug 3628 is fixed.
Bug 3692 is fixed.
Closed bug 3710.
Remaining tactics of the Auto module were put in the monad.
Fix for bug #3618.

Fix typeclass resolution which was considering as subgoals
of a tactic application unrelated pre-existing undefined evars.
Fix ill-typed debugging function
Make use of unfolded primitive projections when elaborating match on a
primitive record.
To stay closer to non-primitive projections, only unfold primitive
projections in cbv when delta _and_ beta flags are set. Add test-suite
file for bug 3700 too.