diff options
| author | Pierre-Marie Pédrot | 2016-03-06 19:01:38 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-06 19:36:03 +0100 |
| commit | 9e96794d6a4327761ce1ff992351199919431be1 (patch) | |
| tree | 389b2b091c2d186490943c6db92c5eaa452bb5f4 /printing | |
| parent | 6ecbc9990a49a0dd51970c7fc8b13f39f02be773 (diff) | |
Moving Tactic_debug to tactics/ folder.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 11 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 5 |
2 files changed, 5 insertions, 11 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index fdc1288aec..7d5e7772c3 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1415,17 +1415,6 @@ let () = let printer _ _ prtac = prtac (0, E) in declare_extra_genarg_pprule wit_tactic printer printer printer -let _ = Hook.set Tactic_debug.tactic_printer - (fun x -> pr_glob_tactic (Global.env()) x) - -let _ = Hook.set Tactic_debug.match_pattern_printer - (fun env sigma hyp -> pr_match_pattern (pr_constr_pattern_env env sigma) hyp) - -let _ = Hook.set Tactic_debug.match_rule_printer - (fun rl -> - pr_match_rule false (pr_glob_tactic (Global.env())) - (fun (_,p) -> pr_constr_pattern p) rl) - module Richpp = struct include Make (Ppconstr.Richpp) (struct diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index c5ec6bb092..b98b6c67e7 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -67,4 +67,9 @@ module type Pp = sig ('constr -> std_ppcmds) -> ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds + val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds + + val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> + ('b, 'a) match_rule -> std_ppcmds + end |