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.
Adding a new intro-pattern for "apply in" on the fly. Using syntax
"pat/term" for "apply term on current_hyp as pat".
Lazy interpretation of patterns so that expressions such as "intros H H'/H"
can be given with second H bound by the first one.

Not very satisfied by passing closure to tactics.ml, but otherwise
tactics would have to be aware of glob_constr.
Fixing unification of subterms identified by patterns.