From 781f44a18cb5e2adbd0b2201d435e27938761af7 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 12 Jun 2013 16:12:32 +0000
Subject: Fixing a Not_found and evar not found anomaly found in ATBR, related
 to setoid_rewrite t where t containts evars, to be added to the goal evars.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16573 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/rewrite.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index e21ee7f23c..679fc8da67 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -375,7 +375,7 @@ let solve_remaining_by by env prf =
 
 let extend_evd sigma ext sigma' =
   Int.Set.fold (fun i acc ->
-    Evd.add acc i (Evd.find sigma' i))
+    Evd.add acc i (Evarutil.nf_evar_info sigma' (Evd.find sigma' i)))
     ext sigma
 
 let no_constraints cstrs = 
-- 
cgit v1.2.3