diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-24 18:22:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-05-03 22:07:44 +0200 |
| commit | 27689bac62f85c039517cbd003f8ea74cb9b4aa7 (patch) | |
| tree | c72c2f3a0af0ed2ddf0dc894aa42b3d5fd75057c /test-suite/output/subst.v | |
| 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 'test-suite/output/subst.v')
| -rw-r--r-- | test-suite/output/subst.v | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v new file mode 100644 index 000000000..e48aa6bb2 --- /dev/null +++ b/test-suite/output/subst.v @@ -0,0 +1,48 @@ +(* Ensure order of hypotheses is respected after "subst" *) + +Set Regular Subst Tactic. +Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True. +intros * Hx Hy Hz H1 HA H2 H3 HB H4. +(* From now on, the order after subst is consistently H1, HA, H2, H3, HB, H4 *) +subst x. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *) +Show. +Undo. +subst y. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *) +Show. +Undo. +subst z. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *) +Show. +Undo. +subst. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *) +(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *) +Show. +trivial. +Qed. + +Unset Regular Subst Tactic. +Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True. +intros * Hx Hy Hz H1 HA H2 H3 HB H4. +subst x. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *) +Show. +Undo. +subst y. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *) +Show. +Undo. +subst z. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *) +Show. +Undo. +subst. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *) +(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *) +Show. +trivial. +Qed. + + |