diff options
| author | Hugo Herbelin | 2014-12-09 12:09:44 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-11 18:34:04 +0100 |
| commit | 34cb1f6491017e4ed1a509f6b83b88a812ac425f (patch) | |
| tree | 0ad12f25af3050bb289147c54fe52f7349f2335e /tactics | |
| parent | d083200ae5b391ceffaa0329a8e3a334036c7968 (diff) | |
Tentatively more informative report of failure when inferring
pattern-matching predicate.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacticals.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 9256e10d60..bb7a3f2e32 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -477,17 +477,16 @@ module New = struct Evd.fold_undefined (fun evk evi acc -> if is_undefined_up_to_restriction sigma evk && not (Evd.mem origsigma evk) then - evi::acc + (evk,evi)::acc else acc) extsigma [] in match rest with | [] -> () - | evi :: _ -> - let (loc,k) = evi.Evd.evar_source in - let evi = Evarutil.nf_evar_info sigma evi in - Pretype_errors.error_unsolvable_implicit loc env sigma evi k None + | (evk,evi) :: _ -> + let (loc,_) = evi.Evd.evar_source in + Pretype_errors.error_unsolvable_implicit loc env sigma evk None let tclWITHHOLES accept_unresolved_holes tac sigma x = tclEVARMAP >>= fun sigma_initial -> |