Continuing r12485-12486 (cleaning around name generation)

- backtrack on incompatibility introduced in intro while trying to
  simplify the condition about when to restart the subscript of a name
  (the legacy says: find a new name from x0 if the name xN exists in
  the context but find a new name from xN+1 if the name xN does not
  exists in the context but is a global to avoid).
- made the names chosen by "intro" compliant with the ones printed in
  the goal and used for "intros until" (possible source of rare
  incompatibilities) [replaced the use of visibly_occur_id for
  printing the goal into a call to next_name_away_in_goal]
- also made the names internal to T in "T -> U" printed the same in
  the goal as they are while printing T after it is introducted in the
  hypotheses [non contravariant propagation of boolean isgoal in
  detype_binder]
- simplified a bit visibly_occur_id (the Rel and Var cases were useless as
  soon as the avoid list contained the current env); still this function is
  costly with polynomial time in the depth of binders
- see file output/Naming.v for examples

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

1 files changed, 96 insertions, 0 deletions

diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out
new file mode 100644
index 000000000..211a16714
--- /dev/null
+++ b/test-suite/output/Naming.out
@@ -0,0 +1,96 @@
+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.
+1 subgoal
+
+  x3 : nat
+  x : nat
+  x1 : nat
+  x4 : nat
+  x0 : nat
+  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)) ->
+   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)) ->
+   x + x1 = x4 + x0 ->
+   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+do 4 intro.
+1 subgoal
+
+  x3 : nat
+  x : nat
+  x1 : nat
+  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)) ->
+   x + x1 = x4 + x0 ->
+   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+do 2 intro.
+1 subgoal
+
+  x3 : nat
+  x : nat
+  x1 : nat
+  x4 : nat
+  x0 : nat
+  H : forall x x3 : nat,
+      x + x1 = x4 + x3 ->
+      forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
+  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
+  x : nat
+  x1 : nat
+  x4 : nat
+  x0 : nat
+  H : forall x x3 : nat,
+      x + x1 = x4 + x3 ->
+      forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
+  H0 : x + x1 = x4 + x0
+  x5 : nat
+  x6 : nat
+  x7 : nat
+  S : nat
+  ============================
+   x5 + S = x6 + x7 + Datatypes.S x