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.out | |
| 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.out')
| -rw-r--r-- | test-suite/output/subst.out | 97 |
1 files changed, 97 insertions, 0 deletions
diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out new file mode 100644 index 000000000..f5768ba44 --- /dev/null +++ b/test-suite/output/subst.out @@ -0,0 +1,97 @@ +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : 0 = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + x, y : nat + Hx : x = 0 + Hy : y = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : y = 3 + HB : True + H4 : 0 = 4 + ============================ + True +1 subgoal + + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : 0 = 3 + HB : True + H4 : 0 = 4 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + HB : True + H4 : z = 4 + H3 : 0 = 3 + ============================ + True +1 subgoal + + x, y : nat + Hx : x = 0 + Hy : y = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : y = 3 + HB : True + H4 : 0 = 4 + ============================ + True +1 subgoal + + HA, HB : True + H4 : 0 = 4 + H3 : 0 = 3 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True |