Merge branch 'v8.6'

1 files changed, 2 insertions, 1 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index aa574e41c5..4101dc23e4 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -468,6 +468,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)
@@ -481,7 +482,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