Removing unused Refiner.tclWITHHOLES.
More self-contained code for tclWITHHOLES.
Fixing too restrictive detection of resolution of evars in "apply in"
(revealed by contribution PTSF).
Better printing of Ltac values.
Removing documentation related to the deprecated State machinery.
Moving the TacExtend node from atomic to plain tactics.

Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
Moving the TacAlias node out of atomic tactics.
Fixing include of debugger.
Fix test-suite file.
Refine patch for behavior of unify_to_subterm to allow backtracking on
unsatisfiable constraint failures but give sensible error messages if
an occurrence was found and only typeclass resolution failed.
Fixes MathClasses.
Fix test-suite files.
Fix test-suite file.
Reorganization of tactics:
- made "apply" tactics of type Proofview.tactic, as well as other inner
  functions about elim and assert
- used same hypothesis naming policy for intros and internal_cut (towards a
  reorganization of intro patterns)
- "apply ... in H as pat" now supports any kind of introduction
  pattern (doc not changed)
Reorganisation of intropattern code
- emphasizing the different kinds of patterns
- factorizing code of the non-naming intro-patterns

Still some questions:

- Should -> and <- apply to hypotheses or not (currently they apply to
  hypotheses either when used in assert-style tactics or apply in, or
  when the term to rewrite is a variable, in which case "subst" is
  applied)?
- Should "subst" be used when the -> or <- rewrites an equation x=t
  posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)?
- Should -> and <- be applicable in non assert-style if the lemma has
  quantifications?
Spotted a source of failure of the constr printer in debugger.
A reorganization of the "assert" tactics (hopefully uniform naming
scheme, redundancies, possibility of chaining a tactic knowing the
name of introduced hypothesis, new proof engine).
Slight simplification of naming of tactics in equality.ml (hopefully).
Isolating a core tactic in replace, shareable to cutrewrite.
A few more comments in tactics.mli and hippatern.ml.
Factorizing cutrewrite (to be made obsolote) and dependent rewrite (to
integrate to "rewrite"?) with the code of "replace".

Incidentally, "inversion" relies on dependent rewrite, with an
incompatibility introduced. Left-to-right rewriting is now done with
"eq_rec_r" while before it was done using "eq_rec" of "eq_sym". The
first one reduces to the second one but simpl is not anymore able to
reduce "eq_rec_r eq_refl". Hopefully cbn is able to do it (see
Zdigits).
Improving error message when applying rewrite to an expression which is not an equality.