Fixing alpha-conversion bug #2723 introduced in r12485-12486.

The optimisation done of Namegen.visibly_occur_id did not preserve
the previous behavior when pr_constr/constr_extern/detype were
called on a term with free rel variables. We backtrack on it to
go back to the 8.2 behavior.

Seized this opportunity to clarify the meaning of the at_top flag
in constrextern.ml and printer.ml and to rename it into
goal_concl_style. The badly-named at_top flag was introduced in
Coq 6.3 in 1999 to mean that when printing variables bound in the
goal, names had to avoid the names of the variables of the goal
context, so as to keep naming stable when using "intro"; in
r4458, printing improved by not avoiding names that were short
names of global definitions, e.g. "S", or "O" (except when the
at_top flag was on for compatibility reasons).

Other printing strategies could be possible in the
non-goal-concl-style mode. For instance, all bound variables
could be made distinct in a given expression, even if no clash
occur, therefore following so-called Barendregt's
convention. This could be done by setting "avoid"
to "ids_of_rel_context (rel_context env)" in extern_constr and
extern_type (and then, Namegen.visibly_occur_id could be
re-simplified again!).

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

3 files changed, 35 insertions, 23 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index dc8957dd4b..99d054e565 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -533,7 +533,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
   buildrec [] [] avoid env construct_nargs branch
 
 and detype_binder isgoal bk avoid env na ty c =
-  let flag = if isgoal then RenamingForGoal else (RenamingElsewhereFor c) in
+  let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (env,c) in
   let na',avoid' =
     if bk = BLetIn then compute_displayed_let_name_in flag avoid na c
     else compute_displayed_name_in flag avoid na c in
@@ -553,9 +553,11 @@ let rec detype_rel_context where avoid env sign =
 	| None -> na,avoid
 	| Some c ->
 	    if b<>None then
-	      compute_displayed_let_name_in (RenamingElsewhereFor c) avoid na c
+	      compute_displayed_let_name_in
+                (RenamingElsewhereFor (env,c)) avoid na c
 	    else
-	      compute_displayed_name_in (RenamingElsewhereFor c) avoid na c in
+	      compute_displayed_name_in
+                (RenamingElsewhereFor (env,c)) avoid na c in
       let b = Option.map (detype false avoid env) b in
       let t = detype false avoid env t in
       (na',Explicit,b,t) :: aux avoid' (add_name na' env) rest
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 0d086919aa..9a1425716f 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -233,22 +233,27 @@ let make_all_name_different env =
    looks for name of same base with lower available subscript beyond current
    subscript *)
 
-let visibly_occur_id id c =
-  let rec occur c = match kind_of_term c with
+let occur_rel p env id =
+  try lookup_name_of_rel p env = Name id
+  with Not_found -> false (* Unbound indice : may happen in debug *)
+
+let visibly_occur_id id (nenv,c) =
+  let rec occur n c = match kind_of_term c with
     | Const _ | Ind _ | Construct _ | Var _
 	  when shortest_qualid_of_global Idset.empty (global_of_constr c)
 	    = qualid_of_ident id -> raise Occur
-    | _ -> iter_constr occur c
+    | Rel p when p>n & occur_rel (p-n) nenv id -> raise Occur
+    | _ -> iter_constr_with_binders succ occur n c
   in
-  try occur c; false
+  try occur 1 c; false
   with Occur -> true
     | Not_found -> false (* Happens when a global is not in the env *)
 
-let next_ident_away_for_default_printing t id avoid =
-  let bad id = List.mem id avoid or visibly_occur_id id t in
+let next_ident_away_for_default_printing env_t id avoid =
+  let bad id = List.mem id avoid or visibly_occur_id id env_t in
   next_ident_away_from id bad
 
-let next_name_away_for_default_printing t na avoid =
+let next_name_away_for_default_printing env_t na avoid =
   let id = match na with
   | Name id   -> id
   | Anonymous ->
@@ -256,7 +261,7 @@ let next_name_away_for_default_printing t na avoid =
       (* taken into account by the function compute_displayed_name_in; *)
       (* just in case, invent a valid name *)
       id_of_string "H" in
-  next_ident_away_for_default_printing t id avoid
+  next_ident_away_for_default_printing env_t id avoid
 
 (**********************************************************************)
 (* Displaying terms avoiding bound variables clashes *)
@@ -279,13 +284,13 @@ let next_name_away_for_default_printing t na avoid =
 type renaming_flags =
   | RenamingForCasesPattern
   | RenamingForGoal
-  | RenamingElsewhereFor of constr
+  | RenamingElsewhereFor of (name list * constr)
 
 let next_name_for_display flags =
   match flags with
   | RenamingForCasesPattern -> next_name_away_in_cases_pattern
   | RenamingForGoal -> next_name_away_in_goal
-  | RenamingElsewhereFor t -> next_name_away_for_default_printing t
+  | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
 let compute_displayed_name_in flags avoid na c =
@@ -307,16 +312,20 @@ let compute_displayed_let_name_in flags avoid na c =
   let fresh_id = next_name_for_display flags na avoid in
   (Name fresh_id, fresh_id::avoid)
 
-let rec rename_bound_vars_as_displayed avoid c =
-  let rec rename avoid c =
+let rec rename_bound_vars_as_displayed avoid env c =
+  let rec rename avoid env c =
     match kind_of_term c with
     | Prod (na,c1,c2)  ->
-	let na',avoid' = compute_displayed_name_in (RenamingElsewhereFor c2) avoid na c2 in
-	mkProd (na', c1, rename avoid' c2)
+	let na',avoid' =
+          compute_displayed_name_in
+            (RenamingElsewhereFor (env,c2)) avoid na c2 in
+	mkProd (na', c1, rename avoid' (add_name na' env) c2)
     | LetIn (na,c1,t,c2) ->
-	let na',avoid' = compute_displayed_let_name_in (RenamingElsewhereFor c2) avoid na c2 in
-	mkLetIn (na',c1,t, rename avoid' c2)
-    | Cast (c,k,t) -> mkCast (rename avoid c, k,t)
+	let na',avoid' =
+          compute_displayed_let_name_in
+            (RenamingElsewhereFor (env,c2)) avoid na c2 in
+	mkLetIn (na',c1,t, rename avoid' (add_name na' env) c2)
+    | Cast (c,k,t) -> mkCast (rename avoid env c, k,t)
     | _ -> c
   in
-  rename avoid c
+  rename avoid env c
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 637cbf64de..6ca0314632 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -70,7 +70,7 @@ val set_reserved_typed_name : (types -> name) -> unit
 type renaming_flags =
   | RenamingForCasesPattern (** avoid only global constructors *)
   | RenamingForGoal (** avoid all globals (as in intro) *)
-  | RenamingElsewhereFor of constr
+  | RenamingElsewhereFor of (name list * constr)
 
 val make_all_name_different : env -> env
 
@@ -80,4 +80,5 @@ val compute_and_force_displayed_name_in :
   renaming_flags -> identifier list -> name -> constr -> name * identifier list
 val compute_displayed_let_name_in :
   renaming_flags -> identifier list -> name -> constr -> name * identifier list
-val rename_bound_vars_as_displayed : identifier list -> types -> types
+val rename_bound_vars_as_displayed :
+  identifier list -> name list -> types -> types