From 1a169b01458829f9420aea9c855b1ef28e5c847d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 26 May 2017 22:34:57 +0200
Subject: Fixing a subtle bug in tclWITHHOLES.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This fixes Théo's bug on eset.
---
 tactics/tacticals.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics/tacticals.ml')

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 66da9ee18..b3655d373 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -487,6 +487,7 @@ module New = struct
 
   let check_evars env sigma extsigma origsigma =
     let rec is_undefined_up_to_restriction sigma evk =
+      if Evd.mem origsigma evk then None else
       let evi = Evd.find sigma evk in
       match Evd.evar_body evi with
       | Evd.Evar_empty -> Some (evk,evi)
@@ -500,7 +501,7 @@ module New = struct
     let rest =
       Evd.fold_undefined (fun evk evi acc ->
         match is_undefined_up_to_restriction sigma evk with
-        | Some (evk',evi) when not (Evd.mem origsigma evk) -> (evk',evi)::acc
+        | Some (evk',evi) -> (evk',evi)::acc
         | _ -> acc)
         extsigma []
     in
-- 
cgit v1.2.3