Infrastructure for fine-grained debug flags

14 files changed, 96 insertions, 123 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 129b220680..6617f4726e 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -19,20 +19,12 @@ open Sorts
 open Constr
 open Context
 open Vars
-open Goptions
 open Tacmach
 open Util
 
 let init_size=5
 
-let cc_verbose=
-  declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Congruence";"Verbose"]
-    ~value:false
-
-let debug x =
-  if cc_verbose () then Feedback.msg_debug (x ())
+let debug_congruence = CDebug.create ~name:"congruence" ()
 
 (* Signature table *)
 
@@ -576,7 +568,7 @@ let add_inst state (inst,int_subst) =
   Control.check_for_interrupt ();
   if state.rew_depth > 0 then
   if is_redundant state inst.qe_hyp_id int_subst then
-    debug (fun () -> str "discarding redundant (dis)equality")
+    debug_congruence (fun () -> str "discarding redundant (dis)equality")
   else
     begin
       Identhash.add state.q_history inst.qe_hyp_id int_subst;
@@ -591,7 +583,7 @@ let add_inst state (inst,int_subst) =
             state.rew_depth<-pred state.rew_depth;
             if inst.qe_pol then
               begin
-                debug (fun () ->
+                debug_congruence (fun () ->
                    (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
                   (str "  [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++
                            pr_term state.env state.sigma s ++ str " == " ++ pr_term state.env state.sigma t ++ str "]"));
@@ -599,7 +591,7 @@ let add_inst state (inst,int_subst) =
               end
             else
               begin
-                debug (fun () ->
+                debug_congruence (fun () ->
                    (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
                   (str "  [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++
                            pr_term state.env state.sigma s ++ str " <> " ++ pr_term state.env state.sigma t ++ str "]"));
@@ -630,7 +622,7 @@ let join_path uf i j=
   min_path (down_path uf i [],down_path uf j [])
 
 let union state i1 i2 eq=
-  debug (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++
+  debug_congruence (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++
                  str " and " ++ pr_idx_term state.env state.sigma state.uf i2 ++ str ".");
   let r1= get_representative state.uf i1
   and r2= get_representative state.uf i2 in
@@ -670,7 +662,7 @@ let union state i1 i2 eq=
         | _,_ -> ()
 
 let merge eq state = (* merge and no-merge *)
-  debug
+  debug_congruence
     (fun () -> str "Merging " ++ pr_idx_term state.env state.sigma state.uf eq.lhs ++
        str " and " ++ pr_idx_term state.env state.sigma state.uf eq.rhs ++ str ".");
   let uf=state.uf in
@@ -683,7 +675,7 @@ let merge eq state = (* merge and no-merge *)
         union state j i (swap eq)
 
 let update t state = (* update 1 and 2 *)
-  debug
+  debug_congruence
     (fun () -> str "Updating term " ++ pr_idx_term state.env state.sigma state.uf t ++ str ".");
   let (i,j) as sign = signature state.uf t in
   let (u,v) = subterms state.uf t in
@@ -745,7 +737,7 @@ let process_constructor_mark t i rep pac state =
             end
 
 let process_mark t m state =
-  debug
+  debug_congruence
     (fun () -> str "Processing mark for term " ++ pr_idx_term state.env state.sigma state.uf t ++ str ".");
   let i=find state.uf t in
   let rep=get_representative state.uf i in
@@ -766,7 +758,7 @@ let check_disequalities state =
           if Int.equal (find uf dis.lhs) (find uf dis.rhs) then (str "Yes", Some dis)
           else (str "No", check_aux q)
         in
-        let _ = debug
+        let _ = debug_congruence
         (fun () -> str "Checking if " ++ pr_idx_term state.env state.sigma state.uf dis.lhs ++ str " = " ++
          pr_idx_term state.env state.sigma state.uf dis.rhs ++ str " ... " ++ info) in
         ans
@@ -953,7 +945,7 @@ let find_instances state =
   let pb_stack= init_pb_stack state in
   let res =ref [] in
   let _ =
-    debug (fun () -> str "Running E-matching algorithm ... ");
+    debug_congruence (fun () -> str "Running E-matching algorithm ... ");
     try
       while true do
         Control.check_for_interrupt ();
@@ -964,7 +956,7 @@ let find_instances state =
     !res
 
 let rec execute first_run state =
-  debug (fun () -> str "Executing ... ");
+  debug_congruence (fun () -> str "Executing ... ");
   try
     while
       Control.check_for_interrupt ();
@@ -974,7 +966,7 @@ let rec execute first_run state =
         None ->
           if not(Int.Set.is_empty state.pa_classes) then
             begin
-              debug (fun () -> str "First run was incomplete, completing ... ");
+              debug_congruence (fun () -> str "First run was incomplete, completing ... ");
               complete state;
               execute false state
             end
@@ -989,12 +981,12 @@ let rec execute first_run state =
                   end
                 else
               begin
-                debug (fun () -> str "Out of instances ... ");
+                debug_congruence (fun () -> str "Out of instances ... ");
                 None
               end
             else
               begin
-                debug (fun () -> str "Out of depth ... ");
+                debug_congruence (fun () -> str "Out of depth ... ");
                 None
               end
       | Some dis -> Some
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 3270f74479..047756deef 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -121,7 +121,7 @@ val term_equal : term -> term -> bool
 
 val constr_of_term : term -> constr
 
-val debug : (unit -> Pp.t) -> unit
+val debug_congruence : CDebug.t
 
 val forest : state -> forest
 
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 53d8c5bdd9..e7e0822916 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -95,13 +95,13 @@ let pinject p c n a =
    p_rule=Inject(p,c,n,a)}
 
 let rec equal_proof env sigma uf i j=
-  debug (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+  debug_congruence (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   if i=j then prefl (term uf i) else
     let (li,lj)=join_path uf i j in
     ptrans (path_proof env sigma uf i li) (psym (path_proof env sigma uf j lj))
 
 and edge_proof env sigma uf ((i,j),eq)=
-  debug (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+  debug_congruence (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let pi=equal_proof env sigma uf i eq.lhs in
   let pj=psym (equal_proof env sigma uf j eq.rhs) in
   let pij=
@@ -117,7 +117,7 @@ and edge_proof env sigma uf ((i,j),eq)=
   ptrans (ptrans pi pij) pj
 
 and constr_proof env sigma uf i ipac=
-  debug (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20));
+  debug_congruence (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20));
   let t=find_oldest_pac uf i ipac in
   let eq_it=equal_proof env sigma uf i t in
   if ipac.args=[] then
@@ -130,20 +130,20 @@ and constr_proof env sigma uf i ipac=
     ptrans eq_it (pcongr p (prefl targ))
 
 and path_proof env sigma uf i l=
-  debug (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++
+  debug_congruence (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++
            (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
   match l with
   | [] -> prefl (term uf i)
   | x::q->ptrans (path_proof env sigma uf (snd (fst x)) q) (edge_proof env sigma uf x)
 
 and congr_proof env sigma uf i j=
-  debug (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+  debug_congruence (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let (i1,i2) = subterms uf i
   and (j1,j2) = subterms uf j in
   pcongr (equal_proof env sigma uf i1 j1) (equal_proof env sigma uf i2 j2)
 
 and ind_proof env sigma uf i ipac j jpac=
-   debug (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+   debug_congruence (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let p=equal_proof env sigma uf i j
   and p1=constr_proof env sigma uf i ipac
   and p2=constr_proof env sigma uf j jpac in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 72f77508d8..341fde7b77 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -420,16 +420,16 @@ let cc_tactic depth additionnal_terms =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     Coqlib.(check_required_library logic_module_name);
-    let _ = debug (fun () -> Pp.str "Reading goal ...") in
+    let _ = debug_congruence (fun () -> Pp.str "Reading goal ...") in
     let state = make_prb gl depth additionnal_terms in
-    let _ = debug (fun () -> Pp.str "Problem built, solving ...") in
+    let _ = debug_congruence (fun () -> Pp.str "Problem built, solving ...") in
     let sol = execute true state in
-    let _ = debug (fun () -> Pp.str "Computation completed.") in
+    let _ = debug_congruence (fun () -> Pp.str "Computation completed.") in
     let uf=forest state in
     match sol with
       None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
     | Some reason ->
-      debug (fun () -> Pp.str "Goal solved, generating proof ...");
+      debug_congruence (fun () -> Pp.str "Goal solved, generating proof ...");
       match reason with
         Discrimination (i,ipac,j,jpac) ->
         let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index d1403558ad..61966b60c0 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -14,7 +14,7 @@ open Pp
 open Lazy
 module NamedDecl = Context.Named.Declaration
 
-let debug = false
+let debug_zify = CDebug.create ~name:"zify" ()
 
 (* The following [constr] are necessary for constructing the proof terms *)
 
@@ -805,12 +805,11 @@ let pp_prf prf =
 
 let interp_prf evd inj source prf =
   let t, prf' = interp_prf evd inj source prf in
-  if debug then
-    Feedback.msg_debug
+  debug_zify (fun () ->
       Pp.(
         str "interp_prf " ++ gl_pr_constr inj.EInjT.inj ++ str " "
         ++ gl_pr_constr source ++ str " = " ++ gl_pr_constr t ++ str " by "
-        ++ gl_pr_constr prf' ++ str " from " ++ pp_prf prf ++ fnl ());
+        ++ gl_pr_constr prf' ++ str " from " ++ pp_prf prf ++ fnl ()));
   (t, prf')
 
 let mkvar evd inj e =
@@ -888,13 +887,12 @@ let app_unop evd src unop arg prf =
 
 let app_unop evd src unop arg prf =
   let res = app_unop evd src unop arg prf in
-  if debug then
-    Feedback.msg_debug
+  debug_zify (fun () ->
       Pp.(
         str "\napp_unop "
         ++ pp_prf evd unop.EUnOpT.inj1_t arg prf
         ++ str " => "
-        ++ pp_prf evd unop.EUnOpT.inj2_t src res);
+        ++ pp_prf evd unop.EUnOpT.inj2_t src res));
   res
 
 let app_binop evd src binop arg1 prf1 arg2 prf2 =
@@ -1066,8 +1064,7 @@ let match_operator env evd hd args (t, d) =
 
 let pp_trans_expr env evd e res =
   let {deriv = inj} = get_injection env evd e.typ in
-  if debug then
-    Feedback.msg_debug Pp.(str "\ntrans_expr " ++ pp_prf evd inj e.constr res);
+  debug_zify (fun () -> Pp.(str "\ntrans_expr " ++ pp_prf evd inj e.constr res));
   res
 
 let declared_term env evd hd args =
@@ -1187,7 +1184,7 @@ let trans_binrel evd src rop a1 prf1 a2 prf2 =
 
 let trans_binrel evd src rop a1 prf1 a2 prf2 =
   let res = trans_binrel evd src rop a1 prf1 a2 prf2 in
-  if debug then Feedback.msg_debug Pp.(str "\ntrans_binrel " ++ pp_prfp res);
+  debug_zify (fun () -> Pp.(str "\ntrans_binrel " ++ pp_prfp res));
   res
 
 let mkprf t p =
@@ -1199,11 +1196,10 @@ let mkprf t p =
 
 let mkprf t p =
   let t', p = mkprf t p in
-  if debug then
-    Feedback.msg_debug
+  debug_zify (fun () ->
       Pp.(
         str "mkprf " ++ gl_pr_constr t ++ str " <-> " ++ gl_pr_constr t'
-        ++ str " by " ++ gl_pr_constr p);
+        ++ str " by " ++ gl_pr_constr p));
   (t', p)
 
 let trans_bin_prop op_constr op_iff t1 p1 t2 p2 =
@@ -1221,7 +1217,7 @@ let trans_bin_prop op_constr op_iff t1 p1 t2 p2 =
 
 let trans_bin_prop op_constr op_iff t1 p1 t2 p2 =
   let prf = trans_bin_prop op_constr op_iff t1 p1 t2 p2 in
-  if debug then Feedback.msg_debug (pp_prfp prf);
+  debug_zify (fun () -> pp_prfp prf);
   prf
 
 let trans_un_prop op_constr op_iff p1 prf1 =
@@ -1285,8 +1281,7 @@ let trans_hyps env evd l =
     [] l
 
 let trans_hyp h t0 prfp =
-  if debug then
-    Feedback.msg_debug Pp.(str "trans_hyp: " ++ pp_prfp prfp ++ fnl ());
+  debug_zify (fun () -> Pp.(str "trans_hyp: " ++ pp_prfp prfp ++ fnl ()));
   match prfp with
   | IProof -> Tacticals.New.tclIDTAC (* Should detect before *)
   | CProof t' ->
@@ -1313,8 +1308,7 @@ let trans_hyp h t0 prfp =
                (tclTHEN (Tactics.clear [h]) (Tactics.rename_hyp [(h', h)])))))
 
 let trans_concl prfp =
-  if debug then
-    Feedback.msg_debug Pp.(str "trans_concl: " ++ pp_prfp prfp ++ fnl ());
+  debug_zify (fun () -> Pp.(str "trans_concl: " ++ pp_prfp prfp ++ fnl ()));
   match prfp with
   | IProof -> Tacticals.New.tclIDTAC
   | CProof t ->
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml
index 1caa042db6..19bdcbac58 100644
--- a/plugins/nsatz/utile.ml
+++ b/plugins/nsatz/utile.ml
@@ -1,9 +1,9 @@
 (* Printing *)
 
 let pr x =
-  if !Flags.debug then (Format.printf "@[%s@]" x; flush(stdout);)else ()
+  if CDebug.(get_flag misc) then (Format.printf "@[%s@]" x; flush(stdout);)else ()
 
 let prt0 s = () (* print_string s;flush(stdout)*)
 
-let sinfo s = if !Flags.debug then Feedback.msg_debug (Pp.str s)
-let info s = if !Flags.debug then Feedback.msg_debug (Pp.str (s ()))
+let sinfo s = if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str s)
+let info s = if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str (s ()))
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)