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

8 files changed, 23 insertions, 44 deletions

diff --git a/CHANGES b/CHANGES
index 627408cc8..0a6ee0d9f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -45,6 +45,9 @@ Tactics
 - Binders given before ":" in lemmas are now automatically
   introduced in the context (possible source of incompatibility that can be
   avoided by unsetting option "Automatic Introduction").
+- Made choice of introduction names compliant with printed names and
+  in particular with "intros until" names (possible source of exceptional
+  incompatibilities).
 
 Tactic Language
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5c910c424..e153bebf4 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -51,8 +51,7 @@ open Genarg
 
 
 let compute_renamed_type gls c =
-  let ids = collect_visible_vars c in
-  rename_bound_vars_as_displayed ids (pf_type_of gls c)
+  rename_bound_vars_as_displayed [] (pf_type_of gls c)
 
 let qed () = Lemmas.save_named true
 let defined () = Lemmas.save_named false
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index aa58a0808..a65cc24ff 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -147,8 +147,7 @@ let mk_clenv_from_n gls n (c,cty) =
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
 let mk_clenv_rename_from_n gls n (c,t) =
-  let ids = collect_visible_vars t in
-  mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed ids t)
+  mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed [] t)
 
 let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 07ac5df21..4de4bde2c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -523,17 +523,6 @@ let collect_metas c =
   in
   List.rev (collrec [] c)
 
-(* collects all visible var occurences (does not include indirect
-   dependencies of section variables via global references) *)
-
-let collect_visible_vars c =
-  let rec collrec acc c =
-    match kind_of_term c with
-    | Var id -> list_add_set id acc
-    | _      -> fold_constr collrec acc c
-  in
-  List.rev (collrec [] c)
-
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 44a96b613..59f7750d3 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -109,7 +109,6 @@ val free_rels : constr -> Intset.t
 val dependent : constr -> constr -> bool
 val dependent_no_evar : constr -> constr -> bool
 val collect_metas : constr -> int list
-val collect_visible_vars : constr -> identifier list
 val occur_term : constr -> constr -> bool (* Synonymous
  of dependent *)
 (* Substitution of metavariables *)
diff --git a/test-suite/check b/test-suite/check
index c5636a820..06df1a12c 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 211a16714..86055c3ba 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 71587e2ee..89e641ac9 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.