diff options
-rw-r--r-- | tactics/tacticals.ml | 17 | ||||
-rw-r--r-- | test-suite/bugs/closed/3896.v | 4 |
2 files changed, 12 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 diff --git a/test-suite/bugs/closed/3896.v b/test-suite/bugs/closed/3896.v new file mode 100644 index 000000000..b433922a2 --- /dev/null +++ b/test-suite/bugs/closed/3896.v @@ -0,0 +1,4 @@ +Goal True. +pose proof 0 as n. +Fail apply pair in n. +(* Used to be an anomaly for a while *) |