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, 3 insertions, 2 deletions

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 315bddd1f..667a0ed43 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -161,8 +161,9 @@ val set_engagement : engagement -> env -> env
 
 (************************************************************************)
 (* Sets of referred section variables *)
-(* [global_vars_set env c] returns the list of [id]'s occurring as
-   [VAR id] in [c] *)
+(* [global_vars_set env c] returns the list of [id]'s occurring either
+   directly as [Var id] in [c] or indirectly as a section variable
+   dependent in a global reference occurring in [c] *)
 val global_vars_set : env -> constr -> Idset.t
 (* the constr must be a global reference *)
 val vars_of_global : env -> constr -> identifier list