Bug Rename

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

1 files changed, 7 insertions, 1 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index da62c1036c..e9e1882f87 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -569,7 +569,13 @@ let prim_refiner r sigma goal =
 (* Util *)
 let rec rebind id1 id2 = function
   | [] -> []
-  | id::l -> if id = id1 then id2::l else id::(rebind id1 id2 l)
+  | id::l -> 
+      if id = id1 then id2::l else
+        let l' = rebind id1 id2 l in
+        if id = id2 then
+          (* TODO: find a more elegant way to hide a variable *)
+          (id_of_string "_@")::l'
+        else id::l'
 
 let prim_extractor subfun vl pft =
   let cl = pft.goal.evar_concl in