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

16 files changed, 119 insertions, 65 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c08972ac1..9bcae183f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -943,21 +943,30 @@ let extern_glob_type vars c =
 
 let loc = dummy_loc (* for constr and pattern, locations are lost *)
 
-let extern_constr_gen at_top scopt env t =
-  let avoid = if at_top then ids_of_context env else [] in
-  let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
+let extern_constr_gen goal_concl_style scopt env t =
+  (* "goal_concl_style" means do alpha-conversion using the "goal" convention *)
+  (* i.e.: avoid using the names of goal/section/rel variables and the short *)
+  (* names of global definitions of current module when computing names for *)
+  (* bound variables. *)
+  (* Not "goal_concl_style" means do alpha-conversion avoiding only *)
+  (* those goal/section/rel variables that occurs in the subterm under *)
+  (* consideration; see namegen.ml for further details *)
+  let avoid = if goal_concl_style then ids_of_context env else [] in
+  let rel_env_names = names_of_rel_context env in
+  let r = Detyping.detype goal_concl_style avoid rel_env_names t in
   let vars = vars_of_env env in
   extern false (scopt,[]) vars r
 
-let extern_constr_in_scope at_top scope env t =
-  extern_constr_gen at_top (Some scope) env t
+let extern_constr_in_scope goal_concl_style scope env t =
+  extern_constr_gen goal_concl_style (Some scope) env t
 
-let extern_constr at_top env t =
-  extern_constr_gen at_top None env t
+let extern_constr goal_concl_style env t =
+  extern_constr_gen goal_concl_style None env t
 
-let extern_type at_top env t =
-  let avoid = if at_top then ids_of_context env else [] in
-  let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
+let extern_type goal_concl_style env t =
+  let avoid = if goal_concl_style then ids_of_context env else [] in
+  let rel_env_names = names_of_rel_context env in
+  let r = Detyping.detype goal_concl_style avoid rel_env_names t in
   extern_glob_type (vars_of_env env) r
 
 let extern_sort s = extern_glob_sort (detype_sort s)
diff --git a/library/impargs.ml b/library/impargs.ml
index b7dbd05fd..6b01c5fb1 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -208,11 +208,10 @@ let rec is_rigid_head t = match kind_of_term t with
 
 (* calcule la liste des arguments implicites *)
 
-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 find_displayed_name_in all avoid na (_,b as envnames_b) =
+  let flag = RenamingElsewhereFor envnames_b in
+  if all then compute_and_force_displayed_name_in flag avoid na b
+  else compute_displayed_name_in flag avoid na b
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rigid = ref true in
@@ -220,7 +219,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env 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 avoid na b in
+	  let na',avoid' = find_displayed_name_in all avoid na (names,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)
       | _ ->
@@ -233,7 +232,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 [] 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
 	!rigid, Array.to_list v
     | _ -> true, []
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 3d2f3e089..dd17ee0c8 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -36,13 +36,19 @@ let delayed_emacs_cmd s =
 (**********************************************************************)
 (** Terms                                                             *)
 
-  (* [at_top] means ids of env must be avoided in bound variables *)
-let pr_constr_core at_top env t =
-  pr_constr_expr (extern_constr at_top env t)
-let pr_lconstr_core at_top env t =
-  pr_lconstr_expr (extern_constr at_top env t)
+(* [goal_concl_style] means that all names of goal/section variables
+   and all names of rel variables (if any) in the given env and all short
+   names of global definitions of the current module must be avoided while
+   printing bound variables.
+   Otherwise, short names of global definitions are printed qualified
+   and only names of goal/section variables and rel names that do
+   _not_ occur in the scope of the binder to be printed are avoided. *)
+
+let pr_constr_core goal_concl_style env t =
+  pr_constr_expr (extern_constr goal_concl_style env t)
+let pr_lconstr_core goal_concl_style env t =
+  pr_lconstr_expr (extern_constr goal_concl_style env t)
 
-let pr_lconstr_env_at_top env = pr_lconstr_core true env
 let pr_lconstr_env env = pr_lconstr_core false env
 let pr_constr_env env = pr_constr_core false env
 
@@ -69,12 +75,12 @@ let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_en
 let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c
 let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c
 
-let pr_type_core at_top env t =
-  pr_constr_expr (extern_type at_top env t)
-let pr_ltype_core at_top env t =
-  pr_lconstr_expr (extern_type at_top env t)
+let pr_type_core goal_concl_style env t =
+  pr_constr_expr (extern_type goal_concl_style env t)
+let pr_ltype_core goal_concl_style env t =
+  pr_lconstr_expr (extern_type goal_concl_style env t)
 
-let pr_ltype_env_at_top env = pr_ltype_core true env
+let pr_goal_concl_style_env env = pr_ltype_core true env
 let pr_ltype_env env = pr_ltype_core false env
 let pr_type_env env = pr_type_core false env
 
@@ -263,7 +269,7 @@ let default_pr_goal gs =
   let preamb,thesis,penv,pc =
     mt (), mt (),
     pr_context_of env,
-    pr_ltype_env_at_top env (Goal.V82.concl sigma g)
+    pr_goal_concl_style_env env (Goal.V82.concl sigma g)
   in
     preamb ++
     str"  " ++ hv 0 (penv ++ fnl () ++
@@ -280,7 +286,7 @@ let pr_goal_tag g =
 let pr_concl n sigma g =
   let (g,sigma) = Goal.V82.nf_evar sigma g in
   let env = Goal.V82.env sigma g in
-  let pc = pr_ltype_env_at_top env (Goal.V82.concl sigma g) in
+  let pc = pr_goal_concl_style_env env (Goal.V82.concl sigma g) in
     str (emacs_str "")  ++
       str "subgoal " ++ int n ++ pr_goal_tag g ++
       str " is:" ++ cut () ++ str" "  ++ pc
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 2d437c201..bbc3a6cad 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -26,7 +26,6 @@ open Tacexpr
 (** Terms *)
 
 val pr_lconstr_env         : env -> constr -> std_ppcmds
-val pr_lconstr_env_at_top  : env -> constr -> std_ppcmds
 val pr_lconstr             : constr -> std_ppcmds
 
 val pr_constr_env          : env -> constr -> std_ppcmds
@@ -44,7 +43,7 @@ val pr_constr_under_binders      : constr_under_binders -> std_ppcmds
 val pr_lconstr_under_binders_env : env -> constr_under_binders -> std_ppcmds
 val pr_lconstr_under_binders     : constr_under_binders -> std_ppcmds
 
-val pr_ltype_env_at_top    : env -> types -> std_ppcmds
+val pr_goal_concl_style_env : env -> types -> std_ppcmds
 val pr_ltype_env           : env -> types -> std_ppcmds
 val pr_ltype               : types -> std_ppcmds
 
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index b5a2ac82e..fd98d5457 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -29,7 +29,7 @@ let pr_goal gs =
     (str "     *** Declarative Mode ***" ++ fnl ()++fnl ()),
     (str "thesis := "  ++ fnl ()),
     Printer.pr_context_of env,
-    Printer.pr_ltype_env_at_top env (Goal.V82.concl sigma g)
+    Printer.pr_goal_concl_style_env env (Goal.V82.concl sigma g)
   in
     preamb ++
     str"  " ++ hv 0 (penv ++ fnl () ++
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 0f92378d6..872d3be4a 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -128,7 +128,8 @@ let pf_get_new_ids idl g =
     []
 
 let compute_renamed_type gls c =
-  rename_bound_vars_as_displayed [] (pf_type_of gls c)
+  rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
+    (pf_type_of gls c)
 let h'_id = id_of_string "h'"
 let heq_id = id_of_string "Heq"
 let teq_id = id_of_string "teq"
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 69b9e6ea7..8415bbd10 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -107,7 +107,7 @@ let pr_context_xml env =
 
 let pr_subgoal_metas_xml metas env=
   let pr_one (meta, typ) =
-    fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_ltype_env_at_top env typ) ++
+    fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_goal_concl_style_env env typ) ++
       str "\"/>"
   in
   List.fold_left (++) (mt ()) (List.map pr_one metas)
@@ -117,7 +117,7 @@ let pr_goal_xml sigma g =
   let env = try Goal.V82.unfiltered_env sigma g with _ -> empty_env in
   if Decl_mode.try_get_info sigma g = None then
     (hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++
-    xmlstream (pr_ltype_env_at_top env (Goal.V82.concl sigma g)) ++
+    xmlstream (pr_goal_concl_style_env env (Goal.V82.concl sigma g)) ++
     str "\"/>" ++
     (pr_context_xml env)) ++
     fnl () ++ str "</goal>")
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index dc8957dd4..99d054e56 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 0d086919a..9a1425716 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 637cbf64d..6ca031463 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
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 417818abf..c4df5721f 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -501,8 +501,8 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
       let clause = mk_clenv_from_env env sigma n (c,t) in
       clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
-      let clause = mk_clenv_from_env env sigma n 
-	(c,rename_bound_vars_as_displayed [] t) 
+      let clause = mk_clenv_from_env env sigma n
+	(c,rename_bound_vars_as_displayed [] [] t)
       in clenv_match_args lbind clause
   | NoBindings ->
       mk_clenv_from_env env sigma n (c,t)
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
new file mode 100644
index 000000000..90ad4ba09
--- /dev/null
+++ b/test-suite/output/names.out
@@ -0,0 +1,5 @@
+The command has indeed failed with message:
+=> Error: In environment
+   y : nat
+   The term "a y" has type "{y0 : nat | y = y0}"
+    while it is expected to have type "{x : nat | x = y}".
diff --git a/test-suite/output/names.v b/test-suite/output/names.v
new file mode 100644
index 000000000..b3b5071a0
--- /dev/null
+++ b/test-suite/output/names.v
@@ -0,0 +1,5 @@
+(* Test no clash names occur *)
+(* see bug #2723 *)
+
+Parameter a : forall x, {y:nat|x=y}.
+Fail Definition b y : {x:nat|x=y} := a y.
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index e3183ef27..8e829e061 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -415,3 +415,17 @@ apply mapfuncomp.
 Abort.
 
 End A.
+
+(* Check "with" clauses refer to names as they are printed *)
+
+Definition hide p := forall n:nat, p = n.
+
+Goal forall n, (forall n, n=0) -> hide n -> n=0.
+unfold hide.
+intros n H H'.
+(* H is displayed as (forall n, n=0) *)
+apply H with (n:=n).
+Undo.
+(* H' is displayed as (forall n0, n=n0) *)
+apply H' with (n0:=0).
+Qed.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4306a9673..a0bffd4fb 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -32,7 +32,6 @@ open Evd
 
 let pr_lconstr c = quote (pr_lconstr c)
 let pr_lconstr_env e c = quote (pr_lconstr_env e c)
-let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c)
 let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t)
 
 let pr_db env i =
@@ -826,8 +825,12 @@ let error_ill_formed_constructor env id c v nparams nargs =
    else
      mt()) ++ str "."
 
+let pr_ltype_using_barendregt_convention_env env c =
+  (* Use goal_concl_style as an approximation of Barendregt's convention (?) *)
+  quote (pr_goal_concl_style_env env c)
+
 let error_bad_ind_parameters env c n v1 v2  =
-  let pc = pr_lconstr_env_at_top env c in
+  let pc = pr_ltype_using_barendregt_convention_env env c in
   let pv1 = pr_lconstr_env env v1 in
   let pv2 = pr_lconstr_env env v2 in
   str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++
@@ -985,7 +988,8 @@ let explain_pattern_matching_error env = function
 
 let explain_reduction_tactic_error = function
   | Tacred.InvalidAbstraction (env,c,(env',e)) ->
-      str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++
+      str "The abstracted term" ++ spc () ++
+      quote (pr_goal_concl_style_env env c) ++
       spc () ++ str "is not well typed." ++ fnl () ++
       explain_type_error env' Evd.empty e
 
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 4f365ebcf..7f01f0307 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -407,7 +407,7 @@ let process_goal sigma g =
   let env = Goal.V82.env sigma g in
   let ccl =
     let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
-    string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in
+    string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in
   let process_hyp h_env d acc =
     let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in
     (string_of_ppcmds (pr_var_decl h_env d)) :: acc in