From 59b4938c3a763e0ed35dd8f91f5d45b286df01a6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 26 Oct 2016 18:32:31 +0200 Subject: TCS: error handling and debug printing in resolution --- tactics/class_tactics.ml | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) (limited to 'tactics') 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 | [] -> -- cgit v1.2.3