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, 7 insertions, 4 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index f82ef03e9..fead921a5 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -200,15 +200,18 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
 
 (* calcule la liste des arguments implicites *)
 
-let find_displayed_name_in all =
-  if all then compute_and_force_displayed_name_in else compute_displayed_name_in
+let find_displayed_name_in all avoid na b =
+  if all then
+    compute_and_force_displayed_name_in (RenamingElsewhereFor b) avoid na b
+  else
+    compute_displayed_name_in (RenamingElsewhereFor b) avoid na b
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rec aux env avoid n names t =
     let t = whd_betadeltaiota env t in
     match kind_of_term t with
       | Prod (na,a,b) ->
-	  let na',avoid' = find_displayed_name_in all None avoid names na b in
+	  let na',avoid' = find_displayed_name_in all avoid na b in
 	  add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
             (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
       | _ ->
@@ -220,7 +223,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   in
   match kind_of_term (whd_betadeltaiota env t) with
     | Prod (na,a,b) ->
-	let na',avoid = find_displayed_name_in all None [] [] na b in
+	let na',avoid = find_displayed_name_in all [] na b in
 	let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
 	Array.to_list v
     | _ -> []