diff options
Diffstat (limited to 'plugins/ltac/tactic_debug.ml')
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 30 |
1 files changed, 12 insertions, 18 deletions
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index e55b49fb4e..99b9e881f6 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -12,7 +12,6 @@ open Util open Names open Pp open Tacexpr -open Termops let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () @@ -51,14 +50,14 @@ let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) let db_pr_goal gl = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let penv = print_named_context env in - let pc = print_constr_env env (Tacmach.New.project gl) concl in + let penv = Termops.Internal.print_named_context env in + let pc = Printer.pr_econstr_env env (Tacmach.New.project gl) concl in str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () let db_pr_goal = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let pg = db_pr_goal gl in Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg)) end @@ -90,7 +89,7 @@ let batch = ref false open Goptions -let _ = +let () = declare_bool_option { optdepr = false; optname = "Ltac batch debug"; @@ -243,7 +242,7 @@ let db_constr debug env sigma c = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Evaluated term: " ++ print_constr_env env sigma c) + msg_tac_debug (str "Evaluated term: " ++ Printer.pr_econstr_env env sigma c) else return () (* Prints the pattern rule *) @@ -268,7 +267,7 @@ let db_matched_hyp debug env sigma (id,_,c) ido = is_debug debug >>= fun db -> if db then msg_tac_debug (str "Hypothesis " ++ Id.print id ++ hyp_bound ido ++ - str " has been matched: " ++ print_constr_env env sigma c) + str " has been matched: " ++ Printer.pr_econstr_env env sigma c) else return () (* Prints the matched conclusion *) @@ -276,7 +275,7 @@ let db_matched_concl debug env sigma c = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env sigma c) + msg_tac_debug (str "Conclusion has been matched: " ++ Printer.pr_econstr_env env sigma c) else return () (* Prints a success message when the goal has been matched *) @@ -366,7 +365,7 @@ let explain_ltac_call_trace last trace loc = Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) - (Tacexpr.TacAtom (Loc.tag te))) + (Tacexpr.TacAtom (CAst.make te))) | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) -> quote (Printer.pr_glob_constr_env (Global.env()) c) ++ (if not (Id.Map.is_empty vars) then @@ -391,19 +390,14 @@ let explain_ltac_call_trace last trace loc = let skip_extensions trace = let rec aux = function - | (_,Tacexpr.LtacNameCall f as tac) :: _ - when Tacenv.is_ltac_for_ml_tactic f -> [tac] - | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: _ -> + | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: tail -> (* Case of an ML defined tactic with entry of the form <<"foo" args>> *) (* see tacextend.mlp *) - [tac] - | (_,Tacexpr.LtacMLCall _ as tac) :: _ -> [tac] + tac :: aux tail | t :: tail -> t :: aux tail | [] -> [] in List.rev (aux (List.rev trace)) -let finer_loc loc1 loc2 = Loc.merge_opt loc1 loc2 = loc2 - let extract_ltac_trace ?loc trace = let trace = skip_extensions trace in let (tloc,c),tail = List.sep_last trace in @@ -411,7 +405,7 @@ let extract_ltac_trace ?loc trace = (* We entered a user-defined tactic, we display the trace with location of the call *) let msg = hov 0 (explain_ltac_call_trace c tail loc ++ fnl()) in - (if finer_loc loc tloc then loc else tloc), Some msg + (if Loc.finer loc tloc then loc else tloc), Some msg else (* We entered a primitive tactic, we don't display trace but report on the finest location *) @@ -420,7 +414,7 @@ let extract_ltac_trace ?loc trace = let rec aux best_loc = function | (loc,_)::tail -> if Option.is_empty best_loc || - not (Option.is_empty loc) && finer_loc loc best_loc + not (Option.is_empty loc) && Loc.finer loc best_loc then aux loc tail else |