diff options
| author | Hugo Herbelin | 2016-04-24 18:22:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-05-03 22:07:44 +0200 |
| commit | 27689bac62f85c039517cbd003f8ea74cb9b4aa7 (patch) | |
| tree | c72c2f3a0af0ed2ddf0dc894aa42b3d5fd75057c /CHANGES | |
| parent | 29697585836c6e0e4d91e28a13c3f40d2137208b (diff) | |
In Regular Subst Tactic mode, ensure that the order of hypotheses is
preserved, which is a source of incompatibilities w.r.t. released 8.5
but which looks to me to be the only possible canonical behavior.
This is I believe a better behavior than the Regular Subst Tactic
behavior in the released 8.5 and 8.5pl1. There, the order of
hypotheses in which substitutions happened was respected, but their
interleaving with other hypotheses was not respected.
So, I consider this to be a fix to the "Regular Subst Tactic" mode.
Also added a more detailed "specification" of the "Regular" behavior
of "subst" in the reference manual.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -4,6 +4,7 @@ Changes from V8.5pl1 to V8.5pl2 Bugfixes - #4677: fix alpha-conversion in notations needing eta-expansion +- Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode. Changes from V8.5 to V8.5pl1 ============================ |