diff options
author | 2014-10-23 18:29:39 +0200 | |
---|---|---|
committer | 2014-10-23 18:46:27 +0200 | |
commit | b5a5253d90275c373c15ff1dd384fea98fe714fd (patch) | |
tree | 247c99ba887801c57253c6aafcf3a60ab250ff0f /test-suite/output/Intuition.out | |
parent | b9e20bbfd6e034f644331b452f67616526fc359f (diff) |
Taking into account factorization of consecutive names of same types
in goal context.
Note: printing of a declaration was previously done in the context
made of the preceding segment of hypotheses, while now it is made in
the full context of all hyps (those coming before and after the hyp
being printed). As a consequence, constants which could be confused
with a variable in the context are now always qualified even if the
conflicting variable name is coming later. But why not, that looks
somehow more uniform like this.
Diffstat (limited to 'test-suite/output/Intuition.out')
-rw-r--r-- | test-suite/output/Intuition.out | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out index 5831c9f43..e99d9fdeb 100644 --- a/test-suite/output/Intuition.out +++ b/test-suite/output/Intuition.out @@ -1,7 +1,6 @@ 1 subgoal - m : Z - n : Z + m, n : Z H : (m >= n)%Z ============================ (m >= m)%Z |