From b5a5253d90275c373c15ff1dd384fea98fe714fd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Oct 2014 18:29:39 +0200
Subject: 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.
---
 test-suite/output/Intuition.out |  3 +--
 test-suite/output/Naming.out    | 34 +++++++---------------------------
 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
-- 
cgit v1.2.3