Addressing report #3279 (inconsistency of behavior of the -> and <-
introduction patterns).

Whether we call -> and <- from assert as or apply in as, or as a
component of a larger introduction pattern, the new documented
semantics is:

- behave as subst if an equation rewriting a variable (rewrite in
  conclusion and hyps and erase variable and hyp).
- rewrite in concl if an equation not rewrite a variable or a
  quantified equality, then erase the hypothesis.

This is potential source of incompatibilities.
Fixing order of hypothesis in goal hypotheses compaction for coqtop.
Documenting some incompatibilities in (non) Import of ML tactics,
Apparently, the former refine was simplifying in hypotheses too.