diff options
| -rw-r--r-- | proofs/logic.ml | 8 |
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 |