diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-22 18:51:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-24 16:44:48 +0200 |
| commit | 5eaa183732bade55d2df3a6173c3765745e6eeb7 (patch) | |
| tree | aec0a68bd96b406ce4dd5e7ef2c5a9e3530a6d4a /CHANGES | |
| parent | d150ef80defc41eb8ed4913ac13e01b04b795ab7 (diff) | |
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.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -198,6 +198,9 @@ Tactics - In destruct/induction, experimental modifier "!" prefixing the hypothesis name to tell not erasing the hypothesis. - Bug fixes in "inversion as" may occasionally lead to incompatibilities. +- Behavior of introduction patterns -> and <- made more uniform + (hypothesis is cleared, rewrite in hypotheses and conclusion and + erasing the variable when rewriting a variable). Program |