Fixing #3896 (incorrect sigma given to printer).

1 files changed, 8 insertions, 9 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5c899aefc..e82af0e2d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -471,22 +471,21 @@ module New = struct
 
   let check_evars env sigma extsigma origsigma =
     let rec is_undefined_up_to_restriction sigma evk =
-      match Evd.evar_body (Evd.find sigma evk) with
-      | Evd.Evar_empty -> true
+      let evi = Evd.find sigma evk in
+      match Evd.evar_body evi with
+      | Evd.Evar_empty -> Some (evk,evi)
       | Evd.Evar_defined c -> match Term.kind_of_term c with
         | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
         | _ -> 
-          (* We make the assumption that there is no way no refine an
+          (* We make the assumption that there is no way to refine an
             evar remaining after typing from the initial term given to
             apply/elim and co tactics, is it correct? *)
-          false in
+          None in
     let rest =
       Evd.fold_undefined (fun evk evi acc ->
-        if is_undefined_up_to_restriction sigma evk && not (Evd.mem origsigma evk)
-        then
-          (evk,evi)::acc
-        else
-          acc)
+        match is_undefined_up_to_restriction sigma evk with
+        | Some (evk',evi) when not (Evd.mem origsigma evk) -> (evk',evi)::acc
+        | _ -> acc)
         extsigma []
     in
     match rest with