diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-23 18:29:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-23 18:46:27 +0200 |
| commit | b5a5253d90275c373c15ff1dd384fea98fe714fd (patch) | |
| tree | 247c99ba887801c57253c6aafcf3a60ab250ff0f /test-suite/output | |
| 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')
| -rw-r--r-- | test-suite/output/Intuition.out | 3 | ||||
| -rw-r--r-- | test-suite/output/Naming.out | 34 | ||||
| -rw-r--r-- | test-suite/output/set.out | 7 |
3 files changed, 10 insertions, 34 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 diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index 105940a45..f0d2562e0 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -6,11 +6,7 @@ (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 1 subgoal - x3 : nat - x : nat - x1 : nat - x4 : nat - x0 : nat + x3, x, x1, x4, x0 : nat H : forall x x3 : nat, x + x1 = x4 + x3 ============================ x + x1 = x4 + x0 @@ -33,11 +29,7 @@ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - x3 : nat - x : nat - x1 : nat - x4 : nat - x0 : nat + x3, x, x1, x4, x0 : nat ============================ (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> @@ -46,11 +38,7 @@ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - x3 : nat - x : nat - x1 : nat - x4 : nat - x0 : nat + x3, x, x1, x4, x0 : nat H : forall x x3 : nat, x + x1 = x4 + x3 -> forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) @@ -59,25 +47,17 @@ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - x3 : nat - x : nat - x1 : nat - x4 : nat - x0 : nat + x3, x, x1, x4, x0 : nat H : forall x x3 : nat, x + x1 = x4 + x3 -> - forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) + forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (Datatypes.S x + x1) H0 : x + x1 = x4 + x0 - x5 : nat - x6 : nat - x7 : nat - S : nat + x5, x6, x7, S : nat ============================ x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - x3 : nat - a : nat + x3, a : nat H : a = 0 -> forall a : nat, a = 0 ============================ a = 0 diff --git a/test-suite/output/set.out b/test-suite/output/set.out index 333fbb86d..4dfd2bc22 100644 --- a/test-suite/output/set.out +++ b/test-suite/output/set.out @@ -6,16 +6,13 @@ x = x 1 subgoal - y1 := 0 : nat - y2 := 0 : nat + y1, y2 := 0 : nat x := y2 + 0 : nat ============================ x = x 1 subgoal - y1 := 0 : nat - y2 := 0 : nat - y3 := 0 : nat + y1, y2, y3 := 0 : nat x := y2 + y3 : nat ============================ x = x |