From 43d4036b7c484768de0c7dc0b7b2a9f3826ac2e8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 23 Sep 2014 22:11:36 +0200
Subject: ATBR can't compile without the fix, as it uses setoid_rewrite to
 rewrite under binders. This might incur a significant time penalty.

---
 tactics/rewrite.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 3feda7b14f..30ee5c5147 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1381,13 +1381,7 @@ let init_hypinfo env sigma c =
       
 let rewrite_with l2r flags c occs : strategy =
   fun () env avoid t ty cstr (sigma, cstrs) ->
-    (** FIXME: This is wrong... the evars in c should not register to the global sigma
-	as the hypothesis might need to be refreshed, e.g. to rewrite under binders
-	and the initial version will not be used while its evars will appear in 
-	the final sigma. Leaving for now to not impact performance, but should be
-	fixed using matching with patterns to avoid costly retypings instead. *)
-    let sigma, hypinfo = decompose_applied_relation_expr env sigma c in
-    let avoid = get_hypinfo_ids hypinfo @ avoid in
+    let hypinfo = init_hypinfo env sigma (Some c) in
     let unify hypinfo env evars t = unify_eqn l2r flags env evars hypinfo None t in
     let app = apply_rule unify occs in
     let strat = 
-- 
cgit v1.2.3