Continuing r12485-12486 and r12549 (cleaning around name generation)

- fixed misunderstanding of the role of nenv while simplifying code of
  occur_id in namegen.ml,
- documented the possible incompatibilites in CHANGES
- fixed output/Naming.v test, and fixed the count of misc. tests in
  test-suite/check.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12556 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 18 insertions, 28 deletions

diff --git a/test-suite/check b/test-suite/check
index c5636a820a..06df1a12cd 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -232,6 +232,7 @@ test_misc () {
     # Non-standard features
 
     # Test xml compilation
+    nbtests=`expr $nbtests + 1`
     printf "    xml..."
     COQ_XML_LIBRARY_ROOT=misc/xml $bincoqc -xml misc/berardi_test > /dev/null 2>&1
     if [ ! -d misc/xml ]; then
diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out
index 211a167145..86055c3baf 100644
--- a/test-suite/output/Naming.out
+++ b/test-suite/output/Naming.out
@@ -1,20 +1,9 @@
-Welcome to Coq localhost:/home/herbelin/coq/git,namegen (cd25d05cf1d1aa17f9c4f90d999559c2e7570b56)
-Parameter x2:nat.
-x2 is assumed
-Definition foo y := forall x x3 x4 S, x + S = x3 + x4 + y.
-foo is defined
-Section A.
-Variable x3:nat.
-x3 is assumed
-Goal forall x x1 x2 x3:nat,
-  (forall x x3:nat, x+x1 = x2+x3) -> x+x1 = x2+x3.
 1 subgoal
 
   x3 : nat
   ============================
    forall x x1 x4 x0 : nat,
-   (forall x5 x6 : nat, x5 + x1 = x4 + x6) -> x + x1 = x4 + x0
-intros.
+   (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
 1 subgoal
 
   x3 : nat
@@ -25,30 +14,23 @@ intros.
   H : forall x x3 : nat, x + x1 = x4 + x3
   ============================
    x + x1 = x4 + x0
-Abort.
-Current goal aborted
-Goal forall x x1 x2 x3:nat,
-  (forall x x3:nat, x+x1 = x2+x3 -> foo (S x + x1)) ->
-   x+x1 = x2+x3 -> foo (S x).
 1 subgoal
 
   x3 : nat
   ============================
    forall x x1 x4 x0 : nat,
-   (forall x5 x6 : nat, x5 + x1 = x4 + x6 -> foo (S x5 + x1)) ->
+   (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
    x + x1 = x4 + x0 -> foo (S x)
-unfold foo.
 1 subgoal
 
   x3 : nat
   ============================
    forall x x1 x4 x0 : nat,
-   (forall x5 x6 : nat,
-    x5 + x1 = x4 + x6 ->
-    forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1)) ->
+   (forall x2 x5 : nat,
+    x2 + x1 = x4 + x5 ->
+    forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
    x + x1 = x4 + x0 ->
    forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
-do 4 intro.
 1 subgoal
 
   x3 : nat
@@ -57,12 +39,11 @@ do 4 intro.
   x4 : nat
   x0 : nat
   ============================
-   (forall x5 x6 : nat,
-    x5 + x1 = x4 + x6 ->
-    forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1)) ->
+   (forall x2 x5 : nat,
+    x2 + x1 = x4 + x5 ->
+    forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
    x + x1 = x4 + x0 ->
    forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
-do 2 intro.
 1 subgoal
 
   x3 : nat
@@ -76,7 +57,6 @@ do 2 intro.
   H0 : x + x1 = x4 + x0
   ============================
    forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
-do 4 intro.
 1 subgoal
 
   x3 : nat
diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v
index 71587e2eef..89e641ac99 100644
--- a/test-suite/output/Naming.v
+++ b/test-suite/output/Naming.v
@@ -7,7 +7,9 @@ Section A.
 Variable x3:nat.
 Goal forall x x1 x2 x3:nat,
   (forall x x3:nat, x+x1 = x2+x3) -> x+x1 = x2+x3.
+Show.
 intros.
+Show.
 
 (* Remark: in V8.2, this used to be printed
 
@@ -37,10 +39,15 @@ Abort.
 Goal forall x x1 x2 x3:nat,
   (forall x x3:nat, x+x1 = x2+x3 -> foo (S x + x1)) ->
    x+x1 = x2+x3 -> foo (S x).
+Show.
 unfold foo.
+Show.
 do 4 intro. (* --> x, x1, x4, x0, ... *)
+Show.
 do 2 intro.
+Show.
 do 4 intro.
+Show.
 
 (* Remark: in V8.2, this used to be printed
 
@@ -71,3 +78,5 @@ before the intros and
    x5 + S = x6 + x7 + Datatypes.S x
 
 after (note the x5/x0 and the S0/S) *)
+
+Abort.