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.

0 files changed, 0 insertions, 0 deletions