diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-26 18:32:31 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-11-03 16:26:39 +0100 |
| commit | 59b4938c3a763e0ed35dd8f91f5d45b286df01a6 (patch) | |
| tree | 7a05b4d1494d5b000211f9a2e2316a1d6d09c3f2 /tactics | |
| parent | ced1e16d43bd896b7e8473921a29749a0ba35643 (diff) | |
TCS: error handling and debug printing in resolution
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 264df5215..8ec005a60 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1044,13 +1044,18 @@ module Search = struct let foundone = ref false in let rec onetac e (tac, pat, b, name, pp) tl = let derivs = path_derivate info.search_cut name in - (if !typeclasses_debug > 1 then - Feedback.msg_debug - (pr_depth (!idx :: info.search_depth) ++ str": trying " ++ + let pr_error ie = + if !typeclasses_debug > 1 then + let msg = + pr_depth (!idx :: info.search_depth) ++ str": " ++ Lazy.force pp ++ (if !foundone != true then str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl) - else mt ()))); + else mt ()) + in + Feedback.msg_debug (msg ++ str " failed with " ++ CErrors.iprint ie) + else () + in let tac_of gls i j = Goal.nf_enter { enter = fun gl' -> let sigma' = Goal.sigma gl' in let s' = Sigma.to_evar_map sigma' in @@ -1136,7 +1141,9 @@ module Search = struct else ortac (with_shelf tac >>= fun s -> let i = !idx in incr idx; result s i None) - (fun e' -> aux (merge_exceptions e e') tl) + (fun e' -> if CErrors.noncritical (fst e') then + (pr_error e'; aux (merge_exceptions e e') tl) + else iraise e') and aux e = function | x :: xs -> onetac e x xs | [] -> |