diff options
Diffstat (limited to 'proofs/tactic_debug.ml')
-rw-r--r-- | proofs/tactic_debug.ml | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 3cc81daf..6d6215c5 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -11,6 +11,7 @@ open Names open Pp open Tacexpr open Termops +open Nameops let (prtac, tactic_printer) = Hook.make () let (prmatchpatt, match_pattern_printer) = Hook.make () @@ -31,7 +32,8 @@ let explain_logic_error = ref (fun e -> mt()) let explain_logic_error_no_anomaly = ref (fun e -> mt()) -let msg_tac_debug s = Proofview.NonLogical.print (s++fnl()) +let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl()) +let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) (* Prints the goal *) @@ -47,7 +49,7 @@ let db_pr_goal gl = let db_pr_goal = Proofview.Goal.nf_enter begin fun gl -> let pg = db_pr_goal gl in - Proofview.tclLIFT (msg_tac_debug (str "Goal:" ++ fnl () ++ pg)) + Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg)) end @@ -120,7 +122,7 @@ let run ini = let open Proofview.NonLogical in if not ini then begin - Proofview.NonLogical.print (str"\b\r\b\r") >> + Proofview.NonLogical.print_notice (str"\b\r\b\r") >> !skipped >>= fun skipped -> msg_tac_debug (str "Executed expressions: " ++ int skipped ++ fnl()) end >> @@ -135,7 +137,7 @@ let rec prompt level = let runtrue = run true in begin let open Proofview.NonLogical in - Proofview.NonLogical.print (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> + Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with @@ -231,17 +233,16 @@ let db_pattern_rule debug num r = (* Prints the hypothesis pattern identifier if it exists *) let hyp_bound = function - | Anonymous -> " (unbound)" - | Name id -> " (bound to "^(Names.Id.to_string id)^")" + | Anonymous -> str " (unbound)" + | Name id -> str " (bound to " ++ pr_id id ++ str ")" (* Prints a matched hypothesis *) let db_matched_hyp debug env (id,_,c) ido = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Hypothesis " ++ - str ((Names.Id.to_string id)^(hyp_bound ido)^ - " has been matched: ") ++ print_constr_env env c) + msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++ + str " has been matched: " ++ print_constr_env env c) else return () (* Prints the matched conclusion *) @@ -266,8 +267,8 @@ let db_hyp_pattern_failure debug env sigma (na,hyp) = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^ - " cannot match: ") ++ + msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++ + str " cannot match: " ++ Hook.get prmatchpatt env sigma hyp) else return () |