diff options
Diffstat (limited to 'plugins/ssr/ssrprinters.ml')
| -rw-r--r-- | plugins/ssr/ssrprinters.ml | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 6ed68094dc..434568b554 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -15,7 +15,6 @@ open Names open Printer open Tacmach -open Ssrmatching_plugin open Ssrast let pr_spc () = str " " @@ -121,15 +120,4 @@ and pr_block = function (Prefix id) -> str"^" ++ Id.print id | (SuffixId id) -> str"^~" ++ Id.print id | (SuffixNum n) -> str"^~" ++ int n -(* 0 cost pp function. Active only if Debug Ssreflect is Set *) -let ppdebug_ref = ref (fun _ -> ()) -let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s) -let () = - Goptions.(declare_bool_option - { optkey = ["Debug";"Ssreflect"]; - optdepr = false; - optread = (fun _ -> !ppdebug_ref == ssr_pp); - optwrite = (fun b -> - Ssrmatching.debug b; - if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) }) -let ppdebug s = !ppdebug_ref s +let debug_ssr = CDebug.create ~name:"ssreflect" () |