Alignement de la politique de renommage de rename_bound_var (utilisé pour

résoudre la clause with de apply/elim) sur la politique de renommage de
concrete_name


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

2 files changed, 22 insertions, 15 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 5c94399336..9b36310c08 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -1034,21 +1034,20 @@ let concrete_let_name avoid_flags l env_names n c =
   let fresh_id = next_name_not_occuring avoid_flags n l env_names c in
   (Name fresh_id, fresh_id::l)
 
-let rec rename_bound_var env l c =
-  match kind_of_term c with
-  | Prod (Name s,c1,c2)  ->
-      if noccurn 1 c2 then
-        let env' = push_rel (Name s,None,c1) env in
-	mkProd (Name s, c1, rename_bound_var env' l c2)
-      else 
-        let s' = next_ident_away s (global_vars env c2@l) in
-        let env' = push_rel (Name s',None,c1) env in
-        mkProd (Name s', c1, rename_bound_var env' (s'::l) c2)
-  | Prod (Anonymous,c1,c2) ->
-        let env' = push_rel (Anonymous,None,c1) env in
-        mkProd (Anonymous, c1, rename_bound_var env' l c2)
-  | Cast (c,k,t) -> mkCast (rename_bound_var env l c, k,t)
-  | x -> c
+let rec rename_bound_var env avoid c =
+  let env_names = names_of_rel_context env in
+  let rec rename avoid c =
+    match kind_of_term c with
+    | Prod (na,c1,c2)  ->
+	let na',avoid' = concrete_name (Some true) avoid env_names na c2 in
+	mkProd (na', c1, rename avoid' c2)
+    | LetIn (na,c1,t,c2) ->
+	let na',avoid' = concrete_let_name (Some true) avoid env_names na c2 in
+	mkLetIn (na',c1,t, rename avoid' c2)
+    | Cast (c,k,t) -> mkCast (rename avoid c, k,t)
+    | _ -> c
+  in
+  rename avoid c
 
 (* Combinators on judgments *)
 
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 454a118d61..3c9fbeb364 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -20,3 +20,11 @@ intros.
 apply n_Sn in H.
 assumption.
 Qed.
+
+(* Check naming in with bindings; printing used to be inconsistent before *)
+(* revision 9450 *)
+
+Notation S':=S (only parsing).
+Goal (forall S, S = S' S) -> (forall S, S = S' S).
+intros.
+apply H with (S0 := S).