aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Naming.out
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-23 18:29:39 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-23 18:46:27 +0200
commitb5a5253d90275c373c15ff1dd384fea98fe714fd (patch)
tree247c99ba887801c57253c6aafcf3a60ab250ff0f /test-suite/output/Naming.out
parentb9e20bbfd6e034f644331b452f67616526fc359f (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/Naming.out')
-rw-r--r--test-suite/output/Naming.out34
1 files changed, 7 insertions, 27 deletions
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