diff options
Diffstat (limited to 'tactics/tacticals.ml')
-rw-r--r-- | tactics/tacticals.ml | 17 |
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 |