diff options
| author | Hugo Herbelin | 2015-01-03 15:55:29 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-03 16:06:46 +0100 |
| commit | 43f01df26be3a3a0f731aeb0728b1b43188a1743 (patch) | |
| tree | 6717f1c2ea6ffc7d5f7090f0d29aab6404d58293 | |
| parent | 893a02f643858ba0b0172648e77af9ccb65f03df (diff) | |
Fixing #3896 (incorrect sigma given to printer).
| -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 5c899aefc2..e82af0e2d1 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 0000000000..b433922a21 --- /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 *) |