A newly introduced variable inside a named context is no longer α-renamed.

Instead, in case of collision, the older name is substituted for a fresh one.
It should also be made inaccessible from the user, but I'll leave this for later.

The goal is to guarantee that [refine (fun x => _)] introduces a binder named [x].

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

3 files changed, 41 insertions, 12 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 8bf1ecf976..ec22bb8fc2 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -303,22 +303,52 @@ let new_untyped_evar =
  *   we have the property that u and phi(t) are convertible in env.
  *)
 
+let subst2 subst vsubst c =
+  substl subst (replace_vars vsubst c)
+
 let push_rel_context_to_named_context env typ =
   (* compute the instances relative to the named context and rel_context *)
   let ids = List.map pi1 (named_context env) in
   let inst_vars = List.map mkVar ids in
   let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
+  let replace_var_named_declaration id0 id (id',b,t) =
+    let id' = if id_ord id0 id' = 0 then id else id' in
+    let vsubst = [id0 , mkVar id] in
+    id', Option.map (replace_vars vsubst) b, replace_vars vsubst t
+  in
+  let replace_var_named_context id0 id  env =
+    let nc = Environ.named_context env in
+    let nc' = List.map (replace_var_named_declaration id0 id) nc in
+    Environ.reset_with_named_context (val_of_named_context nc') env
+  in
+  let extract_if_neq id = function
+    | Anonymous -> None
+    | Name id' when id_ord id id' = 0 -> None
+    | Name id' -> Some id'
+  in
   (* move the rel context to a named context and extend the named instance *)
   (* with vars of the rel context *)
   (* We do keep the instances corresponding to local definition (see above) *)
-  let (subst, _, env) =
+  let (subst, vsubst, _, env) =
     Context.fold_rel_context
-      (fun (na,c,t) (subst, avoid, env) ->
+      (fun (na,c,t) (subst, vsubst, avoid, env) ->
 	let id = next_name_away na avoid in
-	let d = (id,Option.map (substl subst) c,substl subst t) in
-	(mkVar id :: subst, id::avoid, push_named d env))
-      (rel_context env) ~init:([], ids, env) in
-  (named_context_val env, substl subst typ, inst_rels@inst_vars, subst)
+        match extract_if_neq id na with
+        | None ->
+	    let d = (id,Option.map (subst2 subst vsubst) c,subst2 subst vsubst t) in
+	    (mkVar id :: subst, vsubst, id::avoid, push_named d env)
+        | Some id0 ->
+            (* spiwack: if [id<>id0], rather than introducing a new binding
+               named [id], we will keep [id0] (the name given by the user)
+               and rename [id0] into [id] in the named context. *)
+            let subst = List.map (replace_vars [id0,mkVar id]) subst in
+            let vsubst = (id0,mkVar id)::vsubst in
+            let d = (id0, Option.map (subst2 subst vsubst) c, subst2 subst vsubst t) in
+            let env = replace_var_named_context id0  id env in
+            (mkVar id0 :: subst, vsubst, id::avoid, push_named d env)
+      )
+      (rel_context env) ~init:([], [], ids, env) in
+  (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
 
 (*------------------------------------*
  * Entry points to define new evars   *
@@ -344,10 +374,9 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates instance =
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-
 let new_evar evd env ?src ?filter ?candidates typ =
-  let sign,typ',instance,subst = push_rel_context_to_named_context env typ in
-  let candidates = Option.map (List.map (substl subst)) candidates in
+  let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
+  let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
   let instance =
     match filter with
     | None -> instance
@@ -359,7 +388,7 @@ let new_type_evar ?src ?filter evd env =
   new_evar evd' env ?src ?filter (mkSort s)
 
   (* The same using side-effect *)
-let e_new_evar evdref env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?candidates ty =
+let e_new_evar evdref env ?(src=default_source) ?filter ?candidates ty =
   let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
   evdref := evd';
   ev
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index dc4fe0c4bb..05d994f0a6 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -195,6 +195,6 @@ val clear_hyps_in_evi : evar_map ref -> named_context_val -> types ->
   Id.Set.t -> named_context_val * types
 
 val push_rel_context_to_named_context : Environ.env -> types ->
-  named_context_val * types * constr list * constr list
+  named_context_val * types * constr list * constr list * (identifier*constr) list
 
 val generalize_evar_over_rels : evar_map -> existential -> types * constr list
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 0725825e98..c1c1c5f142 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -537,7 +537,7 @@ let evar_dependencies evm p =
     evm ()
 
 let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
-  let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env gl in
+  let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env gl in
   let (gl,t,sigma) =
     Goal.V82.mk_goal sigma nc gl Store.empty in
   let gls = { it = gl ; sigma = sigma; } in