From b54ceca27de0dd2d455ac7f060f897fa67bb8647 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 8 Feb 2003 11:00:32 +0000
Subject: Bug Rename

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3670 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3