diff options
| author | Hugo Herbelin | 2014-10-23 18:29:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-23 18:46:27 +0200 |
| commit | b5a5253d90275c373c15ff1dd384fea98fe714fd (patch) | |
| tree | 247c99ba887801c57253c6aafcf3a60ab250ff0f | |
| 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.
| -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 5831c9f434..e99d9fdebc 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 105940a45d..f0d2562e0f 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 333fbb86d5..4dfd2bc220 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 |