Infrastructure for fine-grained debug flags

8 files changed, 56 insertions, 69 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 4d57abb465..41fd96ccb5 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -252,7 +252,7 @@ let interp_refine ist gl rc =
   in
   let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in
 (*   ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *)
-  ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c));
+  debug_ssr (fun () -> str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c);
   (sigma, (sigma, c))
 
 
@@ -1207,7 +1207,7 @@ let gentac gen =
   Proofview.V82.tactic begin fun gl ->
 (*   ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *)
   let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux gl false gen in
-  ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c));
+  debug_ssr (fun () -> str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c);
   let gl = pf_merge_uc ucst gl in
   if conv
   then tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl)) (old_cleartac clr) gl
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 582c45cde1..78a59abda9 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -126,17 +126,17 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
   fun (oc, orig_clr, occ, c_gen) -> pfLIFT begin fun gl ->
 
   let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in
-  ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM==")));
+  debug_ssr (fun () -> (Pp.str(if is_case then "==CASE==" else "==ELIM==")));
   let fire_subst gl t = Reductionops.nf_evar (project gl) t in
   let is_undef_pat = function
   | sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t)
   | _ -> false in
   let match_pat env p occ h cl =
     let sigma0 = project orig_gl in
-    ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p));
+    debug_ssr (fun () -> Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p));
     let (c,ucst), cl =
       fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in
-    ppdebug(lazy Pp.(str"     got: " ++ pr_constr_env env sigma0 c));
+    debug_ssr (fun () -> Pp.(str"     got: " ++ pr_constr_env env sigma0 c));
     c, EConstr.of_constr cl, ucst in
   let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *)
     let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in
@@ -212,10 +212,10 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
           let renamed_tys =
             Array.mapi (fun j (ctx, cty) ->
               let t = Term.it_mkProd_or_LetIn cty ctx in
-                    ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t));
+                    debug_ssr (fun () -> Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t));
               let t = Arguments_renaming.rename_type t
                 (GlobRef.ConstructRef((kn,i),j+1)) in
-              ppdebug(lazy Pp.(str"Done Search " ++ Printer.pr_constr_env env (project gl) t));
+              debug_ssr (fun () -> Pp.(str"Done Search " ++ Printer.pr_constr_env env (project gl) t));
                 t)
             tys
           in
@@ -241,8 +241,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
   in
   let () =
     let sigma = project gl in
-    ppdebug(lazy Pp.(str"elim= "++ pr_econstr_pat env sigma elim));
-    ppdebug(lazy Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in
+    debug_ssr (fun () -> Pp.(str"elim= "++ pr_econstr_pat env sigma elim));
+    debug_ssr (fun () -> Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in
   let open EConstr in
   let inf_deps_r = match kind_of_type (project gl) elimty with
     | AtomicType (_, args) -> List.rev (Array.to_list args)
@@ -301,7 +301,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
         | Some (c, _, _,gl) -> Some(true, gl)
         | None -> None in
       first [try_c_last_arg;try_c_last_pattern] in
-  ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p));
+  debug_ssr (fun () -> Pp.(str"c_is_head_p= " ++ bool c_is_head_p));
   let gl, predty = pfe_type_of gl pred in
   (* Patterns for the inductive types indexes to be bound in pred are computed
    * looking at the ones provided by the user and the inferred ones looking at
@@ -321,7 +321,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
           loop (patterns @ [i, p, inf_t, occ])
             (clr_t @ clr) (i+1) (deps, inf_deps)
       | [], c :: inf_deps ->
-          ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c));
+          debug_ssr (fun () -> Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c));
           loop (patterns @ [i, mkTpat gl c, c, allocc])
             clr (i+1) ([], inf_deps)
       | _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in
@@ -337,8 +337,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
       loop [] orig_clr (List.length head_p+1) (List.rev deps, inf_deps_r) in
     head_p @ patterns, Util.List.uniquize clr, gl
   in
-  ppdebug(lazy Pp.(pp_concat (str"patterns=") (List.map pp_pat patterns)));
-  ppdebug(lazy Pp.(pp_concat (str"inf. patterns=") (List.map (pp_inf_pat gl) patterns)));
+  debug_ssr (fun () -> Pp.(pp_concat (str"patterns=") (List.map pp_pat patterns)));
+  debug_ssr (fun () -> Pp.(pp_concat (str"inf. patterns=") (List.map (pp_inf_pat gl) patterns)));
   (* Predicate generation, and (if necessary) tactic to generalize the
    * equation asked by the user *)
   let elim_pred, gen_eq_tac, clr, gl =
@@ -348,7 +348,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
     let match_or_postpone (cl, gl, post) (h, p, inf_t, occ) =
       let p = unif_redex gl p inf_t in
       if is_undef_pat p then
-        let () = ppdebug(lazy Pp.(str"postponing " ++ pp_pattern env p)) in
+        let () = debug_ssr (fun () -> Pp.(str"postponing " ++ pp_pattern env p)) in
         cl, gl, post @ [h, p, inf_t, occ]
       else try
         let c, cl, ucst = match_pat env p occ h cl in
@@ -420,8 +420,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
       else gl, concl in
     concl, gen_eq_tac, clr, gl in
   let gl, pty = pf_e_type_of gl elim_pred in
-  ppdebug(lazy Pp.(str"elim_pred=" ++ pp_term gl elim_pred));
-  ppdebug(lazy Pp.(str"elim_pred_ty=" ++ pp_term gl pty));
+  debug_ssr (fun () -> Pp.(str"elim_pred=" ++ pp_term gl elim_pred));
+  debug_ssr (fun () -> Pp.(str"elim_pred_ty=" ++ pp_term gl pty));
   let gl = pf_unify_HO gl pred elim_pred in
   let elim = fire_subst gl elim in
   let gl = pf_resolve_typeclasses ~where:elim ~fail:false gl in
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 0008d31ffd..92a481dd18 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -76,7 +76,7 @@ let simpltac s = Proofview.Goal.enter (fun _ -> simpltac s)
 (** The "congr" tactic *)
 
 let interp_congrarg_at ist gl n rf ty m =
-  ppdebug(lazy Pp.(str"===interp_congrarg_at==="));
+  debug_ssr (fun () -> Pp.(str"===interp_congrarg_at==="));
   let congrn, _ = mkSsrRRef "nary_congruence" in
   let args1 = mkRnat n :: mkRHoles n @ [ty] in
   let args2 = mkRHoles (3 * n) in
@@ -84,7 +84,7 @@ let interp_congrarg_at ist gl n rf ty m =
     if i + n > m then None else
     try
       let rt = mkRApp congrn (args1 @  mkRApp rf (mkRHoles i) :: args2) in
-      ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt));
+      debug_ssr (fun () -> Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt));
       Some (interp_refine ist gl rt)
     with _ -> loop (i + 1) in
   loop 0
@@ -92,8 +92,8 @@ let interp_congrarg_at ist gl n rf ty m =
 let pattern_id = mk_internal_id "pattern value"
 
 let congrtac ((n, t), ty) ist gl =
-  ppdebug(lazy (Pp.str"===congr==="));
-  ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl)));
+  debug_ssr (fun () -> (Pp.str"===congr==="));
+  debug_ssr (fun () -> Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl)));
   let sigma, _ as it = interp_term (pf_env gl) (project gl) ist t in
   let gl = pf_merge_uc_of sigma gl in
   let _, f, _, _ucst = pf_abs_evars gl it in
@@ -124,8 +124,8 @@ let newssrcongrtac arg ist =
   Proofview.Goal.enter_one ~__LOC__ begin fun _g ->
     (Ssrcommon.tacMK_SSR_CONST "ssr_congr_arrow") end >>= fun arr ->
   Proofview.V82.tactic begin fun gl ->
-  ppdebug(lazy Pp.(str"===newcongr==="));
-  ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl)));
+  debug_ssr (fun () -> Pp.(str"===newcongr==="));
+  debug_ssr (fun () -> Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl)));
   (* utils *)
   let fs gl t = Reductionops.nf_evar (project gl) t in
   let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl =
@@ -385,8 +385,8 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
     | Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te)))
     | e when CErrors.noncritical e -> raise (PRtype_error None)
   in
-  ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof));
-  ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty));
+  debug_ssr (fun () -> Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof));
+  debug_ssr (fun () -> Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty));
   try Proofview.V82.of_tactic (refine_with
     ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof)) gl
   with e when CErrors.noncritical e ->
@@ -435,12 +435,12 @@ let rwcltac ?under ?map_redex cl rdx dir sr =
   let sigma0 = Evd.set_universe_context sigma0 ucst in
   let rdxt = Retyping.get_type_of env (fst sr) rdx in
 (*         ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *)
-        ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env env sigma0 (snd sr)));
+        debug_ssr (fun () -> Pp.(str"r@rwcltac=" ++ pr_econstr_env env sigma0 (snd sr)));
   let cvtac, rwtac, sigma0 =
     if EConstr.Vars.closed0 sigma0 r' then
       let sigma, c, c_eq = fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in
       let sigma, c_ty = Typing.type_of env sigma c in
-        ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
+        debug_ssr (fun () -> Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
       let open EConstr in
       match kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
       | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq ->
@@ -521,7 +521,7 @@ let rwprocess_rule env dir rule =
       let t =
         if red = 1 then Tacred.hnf_constr env sigma t0
         else Reductionops.whd_betaiotazeta env sigma t0 in
-      ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t));
+      debug_ssr (fun () -> Pp.(str"rewrule="++pr_econstr_pat env sigma t));
       match EConstr.kind sigma t with
       | Prod (_, xt, at) ->
         let sigma = Evd.create_evar_defs sigma in
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index f2c7f495b3..bc46c23761 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -296,8 +296,8 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave =
       | Some id ->
         if pats = [] then Tacticals.New.tclIDTAC else
         let args = Array.of_list args in
-        ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args))));
-        ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct));
+        debug_ssr (fun () -> str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args)));
+        debug_ssr (fun () -> str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct);
         Tacticals.New.tclTHENS (basecuttac "ssr_have" ct)
           [Tactics.apply EConstr.(mkApp (mkVar id,args)); Tacticals.New.tclIDTAC] in
       "ssr_have",
@@ -395,7 +395,7 @@ let intro_lock ipats =
             Array.length args = 3 && is_app_evar sigma args.(2) ->
           protect_subgoal env sigma hd args
         | _ ->
-    ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t));
+    debug_ssr (fun () -> Pp.(str"under: stop:" ++ pr_econstr_env env sigma t));
 
             Proofview.tclUNIT ()
        end)
@@ -468,13 +468,13 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint =
     | Some l -> [IPatCase(Regular [l;[]])] in
 
   let map_redex env evar_map ~before:_ ~after:t =
-    ppdebug(lazy Pp.(str"under vars: " ++ prlist Names.Name.print varnames));
+    debug_ssr (fun () -> Pp.(str"under vars: " ++ prlist Names.Name.print varnames));
 
     let evar_map, ty = Typing.type_of env evar_map t in
     let new_t = (* pretty-rename the bound variables *)
       try begin match EConstr.destApp evar_map t with (f, ar) ->
             let lam = Array.last ar in
-            ppdebug(lazy Pp.(str"under: mapping:" ++
+            debug_ssr(fun () -> Pp.(str"under: mapping:" ++
                              pr_econstr_env env evar_map lam));
             let new_lam = pretty_rename evar_map lam varnames in
             let new_ar, len1 = Array.copy ar, pred (Array.length ar) in
@@ -482,10 +482,10 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint =
             EConstr.mkApp (f, new_ar)
           end with
       | DestKO ->
-        ppdebug(lazy Pp.(str"under: cannot pretty-rename bound variables with destApp"));
+        debug_ssr (fun () -> Pp.(str"under: cannot pretty-rename bound variables with destApp"));
         t
     in
-    ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t));
+    debug_ssr (fun () -> Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t));
     evar_map, new_t
   in
   let undertacs =
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 1e940b5ad3..f8abed5482 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -324,7 +324,7 @@ end
 `tac`, where k is the size of `seeds` *)
 let tclSEED_SUBGOALS seeds tac =
   tclTHENin tac (fun i n ->
-          Ssrprinters.ppdebug (lazy Pp.(str"seeding"));
+          Ssrprinters.debug_ssr (fun () -> Pp.(str"seeding"));
       (* eg [case: (H _ : nat)] generates 3 goals:
          - 1 for _
          - 2 for the nat constructors *)
@@ -416,11 +416,11 @@ let tclMK_ABSTRACT_VARS ids =
 (* Debugging *)
 let tclLOG p t =
   tclUNIT () >>= begin fun () ->
-    Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ pr_ipatop p));
+    Ssrprinters.debug_ssr (fun () -> Pp.(str "exec: " ++ pr_ipatop p));
     tclUNIT ()
   end <*>
   Goal.enter begin fun g ->
-    Ssrprinters.ppdebug (lazy Pp.(str" on state:" ++ spc () ++
+    Ssrprinters.debug_ssr (fun () -> Pp.(str" on state:" ++ spc () ++
       isPRINT g ++
       str" goal:" ++ spc () ++ Printer.pr_goal (Goal.print g)));
     tclUNIT ()
@@ -429,7 +429,7 @@ let tclLOG p t =
     t p
   >>= fun ret ->
   Goal.enter begin fun g ->
-    Ssrprinters.ppdebug (lazy Pp.(str "done: " ++ isPRINT g));
+    Ssrprinters.debug_ssr (fun () -> Pp.(str "done: " ++ isPRINT g));
     tclUNIT ()
   end
   >>= fun () -> tclUNIT ret
@@ -579,10 +579,10 @@ let tclCompileIPats l =
   elab l
 ;;
 let tclCompileIPats l =
-  Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats input: " ++
+  Ssrprinters.debug_ssr (fun () -> Pp.(str "tclCompileIPats input: " ++
                                   prlist_with_sep spc Ssrprinters.pr_ipat l));
   let ops = tclCompileIPats l in
-  Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats output: " ++
+  Ssrprinters.debug_ssr (fun () -> Pp.(str "tclCompileIPats output: " ++
                                   prlist_with_sep spc pr_ipatop ops));
   ops
 
@@ -597,11 +597,11 @@ let main ?eqtac ~first_case_is_dispatch iops =
 end (* }}} *)
 
 let tclIPAT_EQ eqtac ip =
-  Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
+  Ssrprinters.debug_ssr (fun () -> Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
   IpatMachine.(main ~eqtac ~first_case_is_dispatch:true (tclCompileIPats ip))
 
 let tclIPATssr ip =
-  Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
+  Ssrprinters.debug_ssr (fun () -> Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
   IpatMachine.(main ~first_case_is_dispatch:true (tclCompileIPats ip))
 
 let tclCompileIPats = IpatMachine.tclCompileIPats
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" ()
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index 21fb28038a..994577a0c9 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -51,5 +51,4 @@ val pr_guarded :
 
 val pr_occ : ssrocc -> Pp.t
 
-val ppdebug : Pp.t Lazy.t -> unit
-
+val debug_ssr : CDebug.t
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 97926753f5..b3a9e71a3f 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -194,17 +194,17 @@ let mkGApp f args =
 let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
   let env = Goal.env goal in
   let sigma = Goal.sigma goal in
-  Ssrprinters.ppdebug (lazy
+  Ssrprinters.debug_ssr (fun () ->
     Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env sigma glob));
   try
     let sigma,term = Tacinterp.interp_open_constr ist env sigma (glob,None) in
-    Ssrprinters.ppdebug (lazy
+    Ssrprinters.debug_ssr (fun () ->
       Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term));
     tclUNIT (env,sigma,term)
   with e ->
     (* XXX this is another catch all! *)
     let e, info = Exninfo.capture e in
-    Ssrprinters.ppdebug (lazy
+    Ssrprinters.debug_ssr (fun () ->
     Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env sigma glob));
     tclZERO ~info e
 end
@@ -217,7 +217,7 @@ end
 let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t
 
 let tclADD_CLEAR_IF_ID (env, ist, t) x =
-  Ssrprinters.ppdebug (lazy
+  Ssrprinters.debug_ssr (fun () ->
     Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t));
   let hd, args = EConstr.decompose_app ist t in
   match EConstr.kind ist hd with
@@ -269,11 +269,11 @@ let interp_view ~clear_if_id ist v p =
   let p_id = DAst.make p_id in
   match DAst.get v with
   | Glob_term.GApp (hd, rargs) when is_specialize hd ->
-     Ssrprinters.ppdebug (lazy Pp.(str "specialize"));
+     Ssrprinters.debug_ssr (fun () -> Pp.(str "specialize"));
      interp_glob ist (mkGApp p_id rargs)
      >>= tclKeepOpenConstr >>= tclPAIR []
   | _ ->
-     Ssrprinters.ppdebug (lazy Pp.(str "view"));
+     Ssrprinters.debug_ssr (fun () -> Pp.(str "view"));
      (* We find out how to build (v p) eventually using an adaptor *)
      let adaptors = AdaptorDb.(get Forward) in
      Proofview.tclORELSE
@@ -324,7 +324,7 @@ Goal.enter_one ~__LOC__ begin fun g ->
   let rigid = rigid_of und0 in
   let n, p, to_prune, _ucst = pf_abs_evars2 s0 rigid (sigma, p) in
   let p = if simple_types then pf_abs_cterm s0 n p else p in
-  Ssrprinters.ppdebug (lazy Pp.(str"view@finalized: " ++
+  Ssrprinters.debug_ssr (fun () -> Pp.(str"view@finalized: " ++
     Printer.pr_econstr_env env sigma p));
   let sigma = List.fold_left Evd.remove sigma to_prune in
   Unsafe.tclEVARS sigma <*>
@@ -349,26 +349,26 @@ let rec apply_all_views_aux ~clear_if_id vs finalization conclusion s0 =
                 pose_proof name p <*> conclusion ~to_clear:name) <*>
             tclUNIT false)
   | v :: vs ->
-      Ssrprinters.ppdebug (lazy Pp.(str"piling..."));
+      Ssrprinters.debug_ssr (fun () -> Pp.(str"piling..."));
       is_tac_in_term ~extra_scope:"ssripat" v >>= function
       | `Term v ->
-           Ssrprinters.ppdebug (lazy Pp.(str"..a term"));
+           Ssrprinters.debug_ssr (fun () -> Pp.(str"..a term"));
            pile_up_view ~clear_if_id v <*>
            apply_all_views_aux ~clear_if_id vs finalization conclusion s0
       | `Tac tac ->
-           Ssrprinters.ppdebug (lazy Pp.(str"..a tactic"));
+           Ssrprinters.debug_ssr (fun () -> Pp.(str"..a tactic"));
            finalization s0 (fun name p ->
             (match p with
             | None -> tclUNIT ()
             | Some p -> pose_proof name p) <*>
            Tacinterp.eval_tactic tac <*>
            if vs = [] then begin
-             Ssrprinters.ppdebug (lazy Pp.(str"..was the last view"));
+             Ssrprinters.debug_ssr (fun () -> Pp.(str"..was the last view"));
              conclusion ~to_clear:name <*> tclUNIT true
            end else
              Tactics.clear name <*>
              tclINDEPENDENTL begin
-               Ssrprinters.ppdebug (lazy Pp.(str"..was NOT the last view"));
+               Ssrprinters.debug_ssr (fun () -> Pp.(str"..was NOT the last view"));
                Ssrcommon.tacSIGMA >>=
                  apply_all_views_aux ~clear_if_id vs finalization conclusion
              end >>= reduce_or)