diff options
| author | Pierre-Marie Pédrot | 2016-03-06 23:58:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-06 23:59:18 +0100 |
| commit | ccd7c003ae56a4f7ad600cfc9532651010fb6bf2 (patch) | |
| tree | f867ef6ff857a18554131dd1f0f85df30e25c6d3 /printing | |
| parent | d3653c6da5770dfc4d439639b49193e30172763a (diff) | |
| parent | a9f6f401e66c0bbf0c50801d597cd18097bf91a6 (diff) | |
Partial disentangling of Ltac codebase.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 11 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 5 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 2 |
3 files changed, 5 insertions, 13 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 diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index ffec926a84..a101540aba 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -486,8 +486,6 @@ module Make keyword "Print Hint *" | PrintHintDbName s -> keyword "Print HintDb" ++ spc () ++ str s - | PrintRewriteHintDbName s -> - keyword "Print Rewrite HintDb" ++ spc() ++ str s | PrintUniverses (b, fopt) -> let cmd = if b then "Print Sorted Universes" |