Rework typeclass resolution and control of backtracking.
Add a global option to check for multiple solutions and fail in that
case.
Add another flag to declare classes as having unique instances (not
checked but assumed correct, avoiding some backtracking).
Fix bug #3621, using fold_left2 on arrays of the same size only.
Fix bug #3610, allowing betaiotadelta reduction while unifying types of
records in unification.ml.
Avoid backtracking in typeclass search if a solution for a closed
non-dependent or propositional constraint has already been found
(same behavior as before previous patch).
Fixing bug #3619 in emacs mode.