Merge PR #13202: Infrastructure for fine-grained debug flags

Reviewed-by: gares
Ack-by: herbelin
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Ack-by: ejgallego

54 files changed, 479 insertions, 304 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 1ff1425dea..587bb90d43 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -149,7 +149,7 @@ let remove_load_path dir =
   load_paths := List.filter2 (fun p d -> p <> dir) physical logical
 
 let add_load_path (phys_path,coq_path) =
-  if !Flags.debug then
+  if CDebug.(get_flag misc) then
     Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
            str phys_path);
   let phys_path = CUnix.canonical_path_name phys_path in
diff --git a/checker/checker.ml b/checker/checker.ml
index 3a16b7f407..ba5e3c6d1a 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -130,8 +130,6 @@ let init_load_path () =
   includes := []
 
 
-let set_debug () = Flags.debug := true
-
 let impredicative_set = ref Declarations.PredicativeSet
 let set_impredicative_set () = impredicative_set := Declarations.ImpredicativeSet
 
@@ -218,7 +216,7 @@ let guill s = str "\"" ++ str s ++ str "\""
 let where = function
 | None -> mt ()
 | Some s ->
-  if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
+  if CDebug.(get_flag misc) then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
 
 let explain_exn = function
   | Stream.Failure ->
@@ -247,7 +245,7 @@ let explain_exn = function
     hov 0 (fnl () ++ str "User interrupt.")
   | Univ.UniverseInconsistency i ->
     let msg =
-      if !Flags.debug then
+      if CDebug.(get_flag misc) then
         str "." ++ spc() ++
           Univ.explain_universe_inconsistency Univ.Level.pr i
       else
@@ -335,7 +333,7 @@ let parse_args argv =
     | ("-Q"|"-R") :: d :: p :: rem -> set_include d p;parse rem
     | ("-Q"|"-R") :: ([] | [_]) -> usage ()
 
-    | "-debug" :: rem -> set_debug (); parse rem
+    | "-debug" :: rem -> CDebug.set_debug_all true; parse rem
 
     | "-where" :: _ ->
       Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
@@ -373,7 +371,7 @@ let init_with_argv argv =
   try
     parse_args argv;
     CWarnings.set_flags ("+"^Typeops.warn_bad_relevance_name);
-    if !Flags.debug then Printexc.record_backtrace true;
+    if CDebug.(get_flag misc) then Printexc.record_backtrace true;
     Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
     Flags.if_verbose print_header ();
     init_load_path ();
@@ -388,7 +386,7 @@ let run senv =
     let senv = compile_files senv in
     flush_all(); senv
   with e ->
-    if !Flags.debug then Printexc.print_backtrace stderr;
+    if CDebug.(get_flag misc) then Printexc.print_backtrace stderr;
     fatal_error (explain_exn e) (is_anomaly e)
 
 let start () =
diff --git a/dev/ci/user-overlays/13202-SkySkimmer-debug-infra.sh b/dev/ci/user-overlays/13202-SkySkimmer-debug-infra.sh
new file mode 100644
index 0000000000..d80363c49f
--- /dev/null
+++ b/dev/ci/user-overlays/13202-SkySkimmer-debug-infra.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi debug-infra 13202
diff --git a/doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst b/doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst
new file mode 100644
index 0000000000..cd1ac3a35a
--- /dev/null
+++ b/doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst
@@ -0,0 +1,19 @@
+- **Added:**
+  :opt:`Debug` to control debug messages, functioning similarly to the warning system
+  (`#13202 <https://github.com/coq/coq/pull/13202>`_,
+  by Maxime Dénès and Gaëtan Gilbert).
+  The following flags have been converted (such that ``Set Flag`` becomes ``Set Debug "flag"``):
+
+  - ``Debug Unification`` to ``unification``
+
+  - ``Debug HO Unification`` to ``ho-unification``
+
+  - ``Debug Tactic Unification`` to ``tactic-unification``
+
+  - ``Congruence Verbose`` to ``congruence``
+
+  - ``Debug Cbv`` to ``cbv``
+
+  - ``Debug RAKAM`` to ``RAKAM``
+
+  - ``Debug Ssreflect`` to ``ssreflect``
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 665bae7077..071fcbee11 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -675,10 +675,10 @@ Applying theorems
       :tacn:`notypeclasses refine`: it performs type checking without resolution of
       typeclasses, does not perform beta reductions or shelve the subgoals.
 
-   .. flag:: Debug Unification
-
-      Enables printing traces of unification steps used during
-      elaboration/typechecking and the :tacn:`refine` tactic.
+   :opt:`Debug` ``"unification"`` enables printing traces of
+   unification steps used during elaboration/typechecking and the
+   :tacn:`refine` tactic. ``"ho-unification"`` prints information
+   about higher order heuristics.
 
 .. tacn:: apply @term
    :name: apply
@@ -1040,10 +1040,9 @@ Applying theorems
       when the instantiation of a variable cannot be found
       (cf. :tacn:`eapply` and :tacn:`apply`).
 
-.. flag:: Debug Tactic Unification
-
-   Enables printing traces of unification steps in tactic unification.
-   Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`.
+:opt:`Debug` ``"tactic-unification"`` enables printing traces of
+unification steps in tactic unification. Tactic unification is used in
+tactics such as :tacn:`apply` and :tacn:`rewrite`.
 
 .. _managingthelocalcontext:
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 8db16fff69..37d605360d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -865,6 +865,14 @@ Controlling display
    interpreted from left to right, so in case of an overlap, the flags on the
    right have higher priority, meaning that `A,-A` is equivalent to `-A`.
 
+.. opt:: Debug "{+, {? - } @ident }"
+
+   Configures the display of debug messages. Each :n:`@ident` enables debug messages
+   for that component, while  :n:`-@ident` disables messages for the component.
+   ``all`` activates or deactivates all other components.  ``backtrace`` controls printing of
+   error backtraces.
+
+   :cmd:`Test` `Debug` displays the list of components and their enabled/disabled state.
 .. opt:: Printing Width @natural
 
    This command sets which left-aligned part of the width of the screen is used
diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst
index 5aaded2726..3f1f5d46c5 100644
--- a/doc/sphinx/proofs/automatic-tactics/logic.rst
+++ b/doc/sphinx/proofs/automatic-tactics/logic.rst
@@ -194,9 +194,7 @@ Solvers for logic and equality
       additional arguments can be given to congruence by filling in the holes in the
       terms given in the error message, using the `with` clause.
 
-   .. flag:: Congruence Verbose
-
-      Makes :tacn:`congruence` print debug information.
+   :opt:`Debug` ``"congruence"`` makes :tacn:`congruence` print debug information.
 
 .. tacn:: btauto
 
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index f286533d78..8c000a4aa7 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -559,9 +559,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
       on the profile file to see the results. Consult the ``perf`` documentation
       for more details.
 
-.. flag:: Debug Cbv
-
-   This flag makes :tacn:`cbv` (and its derivative :tacn:`compute`) print
+   :opt:`Debug` ``"Cbv"`` makes :tacn:`cbv` (and its derivative :tacn:`compute`) print
    information about the constants it encounters and the unfolding decisions it
    makes.
 
@@ -662,10 +660,8 @@ the conversion in hypotheses :n:`{+ @ident}`.
    This applies :tacn:`simpl` only to the :n:`{+ @natural}` applicative subterms whose
    head occurrence is :n:`@qualid` (or :n:`@string`).
 
-.. flag:: Debug RAKAM
-
-   This flag makes :tacn:`cbn` print various debugging information.
-   ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine.
+:opt:`Debug` ``"RAKAM"`` makes :tacn:`cbn` print various debugging information.
+``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine.
 
 .. tacn:: unfold @qualid
    :name: unfold
diff --git a/ide/coqide/coqide.ml b/ide/coqide/coqide.ml
index e066fc6292..3fbfbd66d3 100644
--- a/ide/coqide/coqide.ml
+++ b/ide/coqide/coqide.ml
@@ -1374,8 +1374,7 @@ let main files =
 let read_coqide_args argv =
   let set_debug () =
     Minilib.debug := true;
-    Flags.debug := true;
-    Exninfo.record_backtrace true
+    CDebug.set_debug_all true
   in
   let rec filter_coqtop coqtop project_files bindings_files out = function
     |"-unicode-bindings" :: sfilenames :: args ->
diff --git a/ide/coqide/coqide_main.ml b/ide/coqide/coqide_main.ml
index 0812e00960..a178e72806 100644
--- a/ide/coqide/coqide_main.ml
+++ b/ide/coqide/coqide_main.ml
@@ -35,7 +35,7 @@ let catch_gtk_messages () =
         let () = GToolbox.message_box ~title:"Error" (header ^ msg) in
         Coqide.crash_save 1
       |`ERROR ->
-        if !Flags.debug then GToolbox.message_box ~title:"Error" (header ^ msg)
+        if CDebug.(get_flag misc) then GToolbox.message_box ~title:"Error" (header ^ msg)
         else Printf.eprintf "%s\n" (header ^ msg)
       |`DEBUG -> Minilib.log msg
       |level when Sys.os_type = "Win32" -> Minilib.log ~level msg
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index a0a8b71ead..a6a7f7d742 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -35,11 +35,11 @@ let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
 
 let pr_error s = pr_with_pid s
 let pr_debug s =
-  if !Flags.debug then pr_with_pid s
+  if CDebug.(get_flag misc) then pr_with_pid s
 let pr_debug_call q =
-  if !Flags.debug then pr_with_pid ("<-- " ^ Xmlprotocol.pr_call q)
+  if CDebug.(get_flag misc) then pr_with_pid ("<-- " ^ Xmlprotocol.pr_call q)
 let pr_debug_answer q r =
-  if !Flags.debug then pr_with_pid ("--> " ^ Xmlprotocol.pr_full_value q r)
+  if CDebug.(get_flag misc) then pr_with_pid ("--> " ^ Xmlprotocol.pr_full_value q r)
 
 (** Categories of commands *)
 
diff --git a/ide/coqide/microPG.ml b/ide/coqide/microPG.ml
index 5a4871b70a..9908703cea 100644
--- a/ide/coqide/microPG.ml
+++ b/ide/coqide/microPG.ml
@@ -15,7 +15,7 @@ open GdkKeysyms
 open Printf
 
 let eprintf x =
-  if !Flags.debug then Printf.eprintf x else Printf.ifprintf stderr x
+  if CDebug.(get_flag misc) then Printf.eprintf x else Printf.ifprintf stderr x
 
 type gui = {
   notebook : session Wg_Notebook.typed_notebook;
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c19b883e3d..d517d215ed 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -24,6 +24,11 @@ open Environ
 compiler. mllambda represents a fragment of ML, and can easily be printed
 to OCaml code. *)
 
+let debug_native_flag, debug_native_compiler = CDebug.create_full ~name:"native-compiler" ()
+
+let keep_debug_files () =
+  CDebug.get_flag debug_native_flag
+
 (** Local names **)
 
 (* The first component is there for debugging purposes only *)
@@ -1939,7 +1944,7 @@ let compile_constant env sigma con cb =
     | Def t ->
       let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
-      if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code");
+      debug_native_compiler (fun () -> Pp.str "Generated lambda code");
       let is_lazy = is_lazy t in
       let code = if is_lazy then mk_lazy code else code in
       let l = Constant.label con in
@@ -1950,11 +1955,11 @@ let compile_constant env sigma con cb =
           let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in
           (auxdefs,mkMLlam [|univ|] code)
       in
-      if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code");
+      debug_native_compiler (fun () -> Pp.str "Generated mllambda code");
       let code =
         optimize_stk (Glet(Gconstant ("", con),code)::auxdefs)
       in
-      if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code");
+      debug_native_compiler (fun () -> Pp.str "Optimized mllambda code");
       code
     | _ ->
         let i = push_symbol (SymbConst con) in
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index aab6e1d4a0..1b14801fec 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -21,6 +21,10 @@ to OCaml code. *)
 type mllambda
 type global
 
+val debug_native_compiler : CDebug.t
+
+val keep_debug_files : unit -> bool
+
 val pp_global : Format.formatter -> global -> unit
 
 val mk_open : string -> global
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index d77ee759c6..7e73725c6c 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -159,12 +159,12 @@ let native_conv_gen pb sigma env univs t1 t2 =
   let ml_filename, prefix = get_ml_filename () in
   let code, upds = mk_conv_code env sigma prefix t1 t2 in
   let fn = compile ml_filename code ~profile:false in
-  if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
+  debug_native_compiler (fun () -> Pp.str "Running test...");
   let t0 = Sys.time () in
   call_linker ~fatal:true ~prefix fn (Some upds);
   let t1 = Sys.time () in
   let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
-  if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
+  debug_native_compiler (fun () -> Pp.str time_info);
   (* TODO change 0 when we can have de Bruijn *)
   fst (conv_val env pb 0 !rt1 !rt2 univs)
 
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 1e1085d5ff..3eb3c949bc 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -38,7 +38,7 @@ let ( / ) = Filename.concat
 let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "")
 
 let () = at_exit (fun () ->
-    if not !Flags.debug && Lazy.is_val my_temp_dir then
+    if not (keep_debug_files ()) && Lazy.is_val my_temp_dir then
       try
         let d = Lazy.force my_temp_dir in
         Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d);
@@ -129,7 +129,7 @@ let call_compiler ?profile:(profile=false) ml_filename =
        ::"-w"::"a"
        ::include_dirs) @
       ["-impl"; ml_filename] in
-  if !Flags.debug then Feedback.msg_debug (Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args)));
+  debug_native_compiler (fun () -> Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args)));
   try
     let res = CUnix.sys_command (Envars.ocamlfind ()) args in
     match res with
@@ -142,7 +142,7 @@ let call_compiler ?profile:(profile=false) ml_filename =
 let compile fn code ~profile:profile =
   write_ml_code fn code;
   let r = call_compiler ~profile fn in
-  if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn;
+  if (not (keep_debug_files ())) && Sys.file_exists fn then Sys.remove fn;
   r
 
 type native_library = Nativecode.global list * Nativevalues.symbols
@@ -160,7 +160,7 @@ let compile_library (code, symb) fn =
   let fn = dirname / basename in
   write_ml_code fn ~header code;
   let _ = call_compiler fn in
-  if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn
+  if (not (keep_debug_files ())) && Sys.file_exists fn then Sys.remove fn
 
 (* call_linker links dynamically the code for constants in environment or a  *)
 (* conversion test. *)
@@ -171,7 +171,7 @@ let call_linker ?(fatal=true) ~prefix f upds =
     begin
       let msg = "Cannot find native compiler file " ^ f in
       if fatal then CErrors.user_err Pp.(str msg)
-      else if !Flags.debug then Feedback.msg_debug (Pp.str msg)
+      else debug_native_compiler (fun () -> Pp.str msg)
     end
   else
   (try
@@ -180,7 +180,7 @@ let call_linker ?(fatal=true) ~prefix f upds =
    with Dynlink.Error _ as exn ->
      let exn = Exninfo.capture exn in
      if fatal then Exninfo.iraise exn
-     else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn));
+     else debug_native_compiler (fun () -> CErrors.(iprint exn)));
   match upds with Some upds -> update_locations upds | _ -> ()
 
 let link_library ~prefix ~dirname ~basename =
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index c95880dc36..2e27fe071e 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -28,35 +28,35 @@ and translate_field prefix mp env acc (l,x) =
   match x with
   | SFBconst cb ->
      let con = Constant.make2 mp l in
-     (if !Flags.debug then
+     (debug_native_compiler (fun () ->
         let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
-        Feedback.msg_debug (Pp.str msg));
+        Pp.str msg));
      compile_constant_field env prefix con acc cb
   | SFBmind mb ->
-     (if !Flags.debug then
+     (debug_native_compiler (fun () ->
         let id = mb.mind_packets.(0).mind_typename in
         let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in
-        Feedback.msg_debug (Pp.str msg));
+        Pp.str msg));
      compile_mind_field mp l acc mb
   | SFBmodule md ->
      let mp = md.mod_mp in
-     (if !Flags.debug then
+     (debug_native_compiler (fun () ->
         let msg =
           Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
         in
-        Feedback.msg_debug (Pp.str msg));
+        Pp.str msg));
      translate_mod prefix mp env md.mod_type acc
   | SFBmodtype mdtyp ->
      let mp = mdtyp.mod_mp in
-     (if !Flags.debug then
+     (debug_native_compiler (fun () ->
         let msg =
           Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
         in
-        Feedback.msg_debug (Pp.str msg));
+        Pp.str msg));
      translate_mod prefix mp env mdtyp.mod_type acc
 
 let dump_library mp dp env mod_expr =
-  if !Flags.debug then Feedback.msg_debug (Pp.str "Compiling library...");
+  debug_native_compiler (fun () -> Pp.str "Compiling library...");
   match mod_expr with
   | NoFunctor struc ->
       let env = add_structure mp struc empty_delta_resolver env in
diff --git a/lib/cDebug.ml b/lib/cDebug.ml
new file mode 100644
index 0000000000..efa7365b91
--- /dev/null
+++ b/lib/cDebug.ml
@@ -0,0 +1,92 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type flag = bool ref
+
+type t = (unit -> Pp.t) -> unit
+
+let debug = ref CString.Map.empty
+
+(* Used to remember level of Set Debug "all" for debugs created by
+   plugins dynlinked after the Set *)
+let all_flag = ref false
+
+let set_debug_backtrace b =
+  Exninfo.record_backtrace b
+
+let set_debug_all b =
+  set_debug_backtrace b;
+  CString.Map.iter (fun _ flag -> flag := b) !debug;
+  all_flag := b
+
+let create_full ~name () =
+  let anomaly pp = CErrors.anomaly ~label:"CDebug.create" pp in
+  let () = match name with
+    | "all"|"backtrace" -> anomaly Pp.(str"The debug name \""++str name++str"\" is reserved.")
+    | _ ->
+      if CString.Map.mem name !debug then
+        anomaly Pp.(str "The debug name \"" ++ str name ++ str "\" is already used.")
+  in
+  let pp x =
+    Feedback.msg_debug Pp.(str "[" ++ str name ++ str "] " ++ x)
+  in
+  let flag = ref !all_flag in
+  debug := CString.Map.add name flag !debug;
+  let pp x =
+    if !flag
+    then pp (x ())
+  in
+  flag, pp
+
+let create ~name () =
+  snd (create_full ~name ())
+
+let get_flag flag = !flag
+
+let warn_unknown_debug = CWarnings.create ~name:"unknown-debug-flag" ~category:"option"
+    Pp.(fun name -> str "There is no debug flag \"" ++ str name ++ str "\".")
+
+let get_flags () =
+  let pp_flag name flag = if flag then name else "-"^name in
+  let flags =
+    CString.Map.fold
+      (fun name v acc -> pp_flag name !v :: acc)
+      !debug []
+  in
+  let all = pp_flag "all" !all_flag in
+  let bt = pp_flag "backtrace" (Printexc.backtrace_status()) in
+  String.concat "," (all::bt::flags)
+
+exception Error
+
+let parse_flags s =
+  let parse_flag s =
+    if CString.is_empty s then raise Error
+    else if s.[0] = '-'
+    then String.sub s 1 (String.length s - 1), false
+    else s, true
+  in
+  try
+    Some (CList.map parse_flag @@ String.split_on_char ',' s)
+  with Error -> None
+
+let set_flags s = match parse_flags s with
+  | None -> CErrors.user_err Pp.(str "Syntax error in debug flags.")
+  | Some flags ->
+    let set_one_flag (name,b) = match name with
+      | "all" -> set_debug_all b
+      | "backtrace" -> set_debug_backtrace b
+      | _ -> match CString.Map.find_opt name !debug with
+        | None -> warn_unknown_debug name
+        | Some flag -> flag := b
+    in
+    List.iter set_one_flag flags
+
+let misc, pp_misc = create_full ~name:"misc" ()
diff --git a/lib/cDebug.mli b/lib/cDebug.mli
new file mode 100644
index 0000000000..846c4b493b
--- /dev/null
+++ b/lib/cDebug.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type flag
+
+type t = (unit -> Pp.t) -> unit
+
+(** Creates a debug component, which may be used to print debug
+    messages.
+
+    A debug component is named by the string [name]. It is either
+    active or inactive.
+
+    The special component ["all"] may be used to control all components.
+
+    There is also a special component ["backtrace"] to control
+    backtrace recording.
+*)
+val create : name:string -> unit -> t
+
+(** Useful when interacting with a component from code, typically when
+    doing something more complicated than printing.
+
+    Note that the printer function prints some metadata compared to
+    [ fun pp -> if get_flag flag then Feedback.msg_debug (pp ()) ]
+ *)
+val create_full : name:string -> unit -> flag * t
+
+val get_flag : flag -> bool
+
+(** [get_flags] and [set_flags] use the user syntax: a comma separated
+    list of activated "component" and "-component"s. [get_flags] starts
+    with "all" or "-all" and lists all components after it (even if redundant). *)
+val get_flags : unit -> string
+
+(** Components not mentioned are not affected (use the "all" component
+    at the start if you want to reset everything). *)
+val set_flags : string -> unit
+
+val set_debug_all : bool -> unit
+
+val misc : flag
+val pp_misc : t
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 760c07783b..1baedb64c9 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -30,6 +30,7 @@ let anomaly ?loc ?info ?label pp =
   let info = Option.cata (Loc.add_loc info) info loc in
   Exninfo.iraise (Anomaly (label, pp), info)
 
+(* TODO remove the option *)
 exception UserError of string option * Pp.t (* User errors *)
 
 let user_err ?loc ?info ?hdr strm =
@@ -46,7 +47,7 @@ exception Timeout = Control.Timeout
 let where = function
 | None -> mt ()
 | Some s ->
-  if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt ()
+  str "in " ++ str s ++ str ":" ++ spc ()
 
 let raw_anomaly e = match e with
   | Anomaly (s, pps) ->
@@ -133,7 +134,7 @@ let print_no_report e = iprint_no_report (e, Exninfo.info e)
 
 let _ = register_handler begin function
   | UserError(s, pps) ->
-    Some (where s ++ pps)
+    Some pps
   | _ -> None
   end
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 83733cf00d..57e879add7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -46,7 +46,6 @@ let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
 
 let load_vos_libraries = ref false
 
-let debug = ref false
 let xml_debug = ref false
 
 let in_debugger = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index ebd23a4d20..e10e2c8cb8 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -40,7 +40,6 @@ val async_proofs_is_worker : unit -> bool
 val load_vos_libraries : bool ref
 
 (** Debug flags *)
-val debug : bool ref
 val xml_debug : bool ref
 val in_debugger : bool ref
 val in_toplevel : bool ref
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 4e08e87084..bbc9966498 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -10,6 +10,7 @@ Loc
 Feedback
 CErrors
 CWarnings
+CDebug
 
 AcyclicGraph
 Rtree
diff --git a/lib/spawn.ml b/lib/spawn.ml
index 2fe7b31d04..27b4387b61 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -13,7 +13,7 @@ let prefer_sock = Sys.os_type = "Win32"
 let accept_timeout = 10.0
 
 let pr_err s = Printf.eprintf "(Spawn  ,%d) %s\n%!" (Unix.getpid ()) s
-let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+let prerr_endline s = if CDebug.(get_flag misc) then begin pr_err s end else ()
 
 type req = ReqDie | Hello of int * int
 
diff --git a/library/nametab.ml b/library/nametab.ml
index e94b696b60..bd96446f1c 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -574,7 +574,7 @@ let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
   with Not_found as exn ->
     let exn, info = Exninfo.capture exn in
-    if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found");
+    if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str "pr_global_env not found");
     Exninfo.iraise (exn, info)
 
 let global_inductive qid =
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)
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 7930c3d634..02fb347d08 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -201,10 +201,7 @@ let cofixp_reducible flgs _ stk =
   else
     false
 
-let get_debug_cbv = Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~value:false
-    ~key:["Debug";"Cbv"]
+let debug_cbv = CDebug.create ~name:"Cbv" ()
 
 (* Reduction of primitives *)
 
@@ -525,7 +522,7 @@ and norm_head_ref k info env stack normt t =
   if red_set_ref info.reds normt then
     match cbv_value_cache info normt with
       | Declarations.Def body ->
-         if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt);
+         debug_cbv (fun () -> Pp.(str "Unfolding " ++ debug_pr_key normt));
          strip_appl (shift_value k body) stack
       | Declarations.Primitive op ->
         let c = match normt with
@@ -534,11 +531,11 @@ and norm_head_ref k info env stack normt t =
         in
         (PRIMITIVE(op,c,[||]),stack)
       | Declarations.OpaqueDef _ | Declarations.Undef _ ->
-         if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
+         debug_cbv (fun () -> Pp.(str "Not unfolding " ++ debug_pr_key normt));
          (VAL(0,make_constr_ref k normt t),stack)
   else
     begin
-      if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
+      debug_cbv (fun () -> Pp.(str "Not unfolding " ++ debug_pr_key normt));
       (VAL(0,make_constr_ref k normt t),stack)
     end
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 990e84e5a7..e1d6fff3e4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -47,17 +47,9 @@ let default_flags env =
   let ts = default_transparent_state env in
   default_flags_of ts
 
-let debug_unification =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Debug";"Unification"]
-    ~value:false
-
-let debug_ho_unification =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Debug";"HO";"Unification"]
-    ~value:false
+let debug_unification = CDebug.create ~name:"unification" ()
+
+let debug_ho_unification = CDebug.create ~name:"ho-unification" ()
 
 (*******************************************)
 (* Functions to deal with impossible cases *)
@@ -808,9 +800,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
   in
   let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
   (* Evar must be undefined since we have flushed evars *)
-  let () = if debug_unification () then
-             let open Pp in
-             Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
+  let () = debug_unification (fun () -> Pp.(v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ()))) in
   match (flex_kind_of_term flags env evd term1 sk1,
          flex_kind_of_term flags env evd term2 sk2) with
     | Flexible (sp1,al1), Flexible (sp2,al2) ->
@@ -1288,17 +1278,17 @@ let apply_on_subterm env evd fixed f test c t =
               (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
               applyrec acc t
     else
-    (if debug_ho_unification () then
-     Feedback.msg_debug Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t);
+    (debug_ho_unification (fun () ->
+     Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t));
      let b, evd =
         try test env !evdref k c t
         with e when CErrors.noncritical e -> assert false in
-     if b then (if debug_ho_unification () then Feedback.msg_debug (Pp.str "succeeded");
+     if b then (debug_ho_unification (fun () -> Pp.str "succeeded");
                 let evd', fixed, t' = f !evdref !fixedref k t in
                 fixedref := fixed;
                 evdref := evd'; t')
      else (
-       if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed");
+       debug_ho_unification (fun () -> Pp.str "failed");
        map_constr_with_binders_left_to_right env !evdref
         (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
         applyrec acc t))
@@ -1404,9 +1394,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   let env_evar = evar_filtered_env env_rhs evi in
   let sign = named_context_val env_evar in
   let ctxt = evar_filtered_context evi in
-  if debug_ho_unification () then
-    (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs);
-     Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar));
+  debug_ho_unification (fun () ->
+     Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs ++ fnl () ++
+         str"env evars: " ++ Termops.Internal.print_env env_evar));
   let args = List.map (nf_evar evd) args in
   let argsubst = List.map2 (fun decl c -> (NamedDecl.get_id decl, c)) ctxt args in
   let instance = evar_identity_subst evi in
@@ -1439,17 +1429,17 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   let rec set_holes env_rhs evd fixed rhs = function
   | (id,idty,c,cty,evsref,filter,occs)::subst ->
      let c = nf_evar evd c in
-     if debug_ho_unification () then
-       Feedback.msg_debug Pp.(str"set holes for: " ++
+     debug_ho_unification (fun () ->
+       Pp.(str"set holes for: " ++
                                 prc env_rhs evd (mkVar id.binder_name) ++ spc () ++
                                 prc env_rhs evd c ++ str" in " ++
-                                prc env_rhs evd rhs);
+                                prc env_rhs evd rhs));
      let occ = ref 1 in
      let set_var evd fixed k inst =
        let oc = !occ in
-       if debug_ho_unification () then
-       (Feedback.msg_debug Pp.(str"Found one occurrence");
-        Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs evd c));
+       debug_ho_unification (fun () ->
+       Pp.(str"Found one occurrence" ++ fnl () ++
+           str"cty: " ++ prc env_rhs evd c));
        incr occ;
        match occs with
        | AtOccurrences occs ->
@@ -1458,10 +1448,10 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
        | Unspecified prefer_abstraction ->
           let evd, fixed, evty = set_holes env_rhs evd fixed cty subst in
           let evty = nf_evar evd evty in
-          if debug_ho_unification () then
-            Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++
-                                   str" of type: " ++ prc env_evar evd evty ++
-                                   str " for " ++ prc env_rhs evd c);
+          debug_ho_unification (fun () ->
+            Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++
+                str" of type: " ++ prc env_evar evd evty ++
+                str " for " ++ prc env_rhs evd c));
           let instance = Filter.filter_list filter instance in
           (* Allow any type lower than the variable's type as the
              abstracted subterm might have a smaller type, which could be
@@ -1477,8 +1467,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
           evd, fixed, mkEvar (evk, instance)
      in
      let evd, fixed, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in
-     if debug_ho_unification () then
-       Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs');
+     debug_ho_unification (fun () ->
+       Pp.(str"abstracted: " ++ prc env_rhs evd rhs'));
      let () = check_selected_occs env_rhs evd c !occ occs in
      let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in
      set_holes env_rhs' evd fixed rhs' subst
@@ -1491,9 +1481,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   (* Thin evars making the term typable in env_evar *)
   let evd, rhs' = thin_evars env_evar evd ctxt rhs' in
   (* We instantiate the evars of which the value is forced by typing *)
-  if debug_ho_unification () then
-    (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs');
-     Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
+  debug_ho_unification (fun () ->
+    Pp.(str"solve_evars on: " ++ prc env_evar evd rhs' ++ fnl () ++
+        str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
   let evd,rhs' =
     try !solve_evars env_evar evd rhs'
     with e when Pretype_errors.precatchable_exception e ->
@@ -1501,18 +1491,18 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
       raise (TypingFailed evd) in
   let rhs' = nf_evar evd rhs' in
   (* We instantiate the evars of which the value is forced by typing *)
-  if debug_ho_unification () then
-    (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs');
-     Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
+  debug_ho_unification (fun () ->
+    Pp.(str"after solve_evars: " ++ prc env_evar evd rhs' ++ fnl () ++
+    str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
 
   let rec abstract_free_holes evd = function
    | (id,idty,c,cty,evsref,_,_)::l ->
      let id = id.binder_name in
      let c = nf_evar evd c in
-     if debug_ho_unification () then
-       Feedback.msg_debug Pp.(str"abstracting: " ++
-                                prc env_rhs evd (mkVar id) ++ spc () ++
-                                prc env_rhs evd c);
+     debug_ho_unification (fun () ->
+       Pp.(str"abstracting: " ++
+             prc env_rhs evd (mkVar id) ++ spc () ++
+             prc env_rhs evd c));
      let rec force_instantiation evd = function
      | (evk,evty,inst,abstract)::evs ->
        let evk = Option.default evk (Evarutil.advance evd evk) in
@@ -1541,14 +1531,14 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
            with IllTypedInstance _ (* from instantiate_evar *) | TypingFailed _ ->
               user_err (Pp.str "Cannot find an instance.")
          else
-           ((if debug_ho_unification () then
+           ((debug_ho_unification (fun () ->
                let evi = Evd.find evd evk in
                let env = Evd.evar_env env_rhs evi in
-               Feedback.msg_debug Pp.(str"evar is defined: " ++
+               Pp.(str"evar is defined: " ++
                  int (Evar.repr evk) ++ spc () ++
                  prc env evd (match evar_body evi with Evar_defined c -> c
                    | Evar_empty -> assert false)));
-            evd)
+            evd))
        in force_instantiation evd evs
      | [] -> abstract_free_holes evd l
      in force_instantiation evd !evsref
@@ -1556,27 +1546,27 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
      if Evd.is_defined evd evk then
        (* Can happen due to dependencies: instantiating evars in the arguments of evk might
            instantiate evk itself. *)
-       (if debug_ho_unification () then
+       (debug_ho_unification (fun () ->
           begin
             let evi = Evd.find evd evk in
             let evenv = evar_env env_rhs evi in
             let body = match evar_body evi with Evar_empty -> assert false | Evar_defined c -> c in
-            Feedback.msg_debug Pp.(str"evar was defined already as: " ++ prc evenv evd body)
-          end;
+            Pp.(str"evar was defined already as: " ++ prc evenv evd body)
+          end);
         evd)
      else
        try
          let evi = Evd.find_undefined evd evk in
          let evenv = evar_env env_rhs evi in
          let rhs' = nf_evar evd rhs' in
-           if debug_ho_unification () then
-             Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++
-                                      prc evenv evd rhs');
+           debug_ho_unification (fun () ->
+             Pp.(str"abstracted type before second solve_evars: " ++
+                   prc evenv evd rhs'));
          (* solve_evars is not commuting with nf_evar, because restricting
              an evar might provide a more specific type. *)
           let evd, _ = !solve_evars evenv evd rhs' in
-          if debug_ho_unification () then
-            Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs'));
+          debug_ho_unification (fun () ->
+            Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs')));
           let flags = default_flags_of TransparentState.full in
             Evarsolve.instantiate_evar evar_unify flags env_rhs evd evk rhs'
          with IllTypedInstance _ -> raise (TypingFailed evd)
@@ -1629,11 +1619,10 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
   let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in
   let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in
   let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in
-  let () = if debug_unification () then
-             let open Pp in
-             Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++
+  let () = debug_unification (fun () ->
+             Pp.(v 0 (str "Heuristic:" ++ spc () ++
                                 Termops.Internal.print_constr_env env evd t1 ++ cut () ++
-                                Termops.Internal.print_constr_env env evd t2 ++ cut ())) in
+                                Termops.Internal.print_constr_env env evd t2 ++ cut ()))) in
   let app_empty = Array.is_empty l1 && Array.is_empty l2 in
   match EConstr.kind evd term1, EConstr.kind evd term2 with
   | Evar (evk1,args1), (Rel _|Var _) when app_empty
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 92e412a537..28621aa92e 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -469,15 +469,15 @@ let start_profiler_linux profile_fn =
       Unix.stdin dev_null dev_null
   in
   (* doesn't seem to be a way to test whether process creation succeeded *)
-  if !Flags.debug then
-    Feedback.msg_debug (Pp.str (Format.sprintf "Native compute profiler started, pid = %d, output to: %s" profiler_pid profile_fn));
+  debug_native_compiler (fun () ->
+    Pp.str (Format.sprintf "Native compute profiler started, pid = %d, output to: %s" profiler_pid profile_fn));
   Some profiler_pid
 
 (* kill profiler via SIGINT *)
 let stop_profiler_linux m_pid =
   match m_pid with
   | Some pid -> (
-    let _ = if !Flags.debug then Feedback.msg_debug (Pp.str "Stopping native code profiler") in
+    let _ = debug_native_compiler (fun () -> Pp.str "Stopping native code profiler") in
     try
       Unix.kill pid Sys.sigint;
       let _ = Unix.waitpid [] pid in ()
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 54a47a252d..4083d3bc23 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -686,11 +686,7 @@ module CredNative = RedNative(CNativeEntries)
     contract_* in any case .
 *)
 
-let debug_RAKAM =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Debug";"RAKAM"]
-    ~value:false
+let debug_RAKAM = CDebug.create ~name:"RAKAM" ()
 
 let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
   let args = Stack.tail ci.ci_npar args in
@@ -709,18 +705,18 @@ let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
 let rec whd_state_gen flags env sigma =
   let open Context.Named.Declaration in
   let rec whrec (x, stack) : state =
-    let () = if debug_RAKAM () then
+    let () =
         let open Pp in
         let pr c = Termops.Internal.print_constr_env env sigma c in
-        Feedback.msg_debug
+        debug_RAKAM (fun () ->
                (h (str "<<" ++ pr x ++
                    str "|" ++ cut () ++ Stack.pr pr stack ++
-                   str ">>"))
+                   str ">>")))
     in
     let c0 = EConstr.kind sigma x in
     let fold () =
-      let () = if debug_RAKAM () then
-          let open Pp in Feedback.msg_debug (str "<><><><><>") in
+      let () = debug_RAKAM (fun () ->
+          let open Pp in str "<><><><><>") in
       ((EConstr.of_kind c0, stack))
     in
     match c0 with
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 41d16f1c3c..09bcc860d0 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -19,7 +19,7 @@ open Environ
 
 exception Elimconst
 
-val debug_RAKAM : unit -> bool
+val debug_RAKAM : CDebug.t
 
 module CredNative : Primred.RedNative with
   type elem = EConstr.t and type args = EConstr.t array and type evd = Evd.evar_map
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 83e46e3295..df0f49a033 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -49,11 +49,7 @@ let is_keyed_unification =
     ~key:["Keyed";"Unification"]
     ~value:false
 
-let debug_unification =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Debug";"Tactic";"Unification"]
-    ~value:false
+let debug_tactic_unification = CDebug.create ~name:"tactic-unification" ()
 
 (** Making this unification algorithm correct w.r.t. the evar-map abstraction
     breaks too much stuff. So we redefine incorrect functions here. *)
@@ -713,8 +709,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     let cM = Evarutil.whd_head_evar sigma curm
     and cN = Evarutil.whd_head_evar sigma curn in
     let () =
-      if debug_unification () then
-        Feedback.msg_debug (
+      debug_tactic_unification (fun () ->
           Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++
           Termops.Internal.print_constr_env curenv sigma cN)
     in
@@ -1138,7 +1133,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
   in
 
-  if debug_unification () then Feedback.msg_debug (str "Starting unification");
+  debug_tactic_unification (fun () -> str "Starting unification");
   let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in
   try
   let res =
@@ -1165,11 +1160,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     let a = match res with
     | Some sigma -> sigma, ms, es
     | None -> unirec_rec (env,0) cv_pb opt subst (fst m) (fst n) in
-    if debug_unification () then Feedback.msg_debug (str "Leaving unification with success");
+    debug_tactic_unification (fun () -> str "Leaving unification with success");
     a
   with e ->
     let e = Exninfo.capture e in
-    if debug_unification () then Feedback.msg_debug (str "Leaving unification with failure");
+    debug_tactic_unification (fun () -> str "Leaving unification with failure");
     Exninfo.iraise e
 
 let unify_0 env sigma pb flags c1 c2 =
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 4c4c26f47e..dd80ff21aa 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -13,7 +13,7 @@ open Pp
 open Util
 
 let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp
-let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else ()
+let stm_prerr_endline s = if CDebug.(get_flag misc) then begin stm_pr_err (str s) end else ()
 
 type cancel_switch = bool ref
 let async_proofs_flags_for_workers = ref []
diff --git a/stm/spawned.ml b/stm/spawned.ml
index 5cc8be78f5..ee9c8e9942 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -11,7 +11,7 @@
 open Spawn
 
 let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s
-let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+let prerr_endline s = if CDebug.(get_flag misc) then begin pr_err s end else ()
 
 type chandescr = AnonPipe | Socket of string * int * int
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 7de109e596..5ed6adbd63 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 (* enable in case of stm problems  *)
-(* let stm_debug () = !Flags.debug *)
+(* let stm_debug () = CDebug.(get_flag misc) *)
 let stm_debug = ref false
 
 let stm_pr_err s  = Format.eprintf "%s] %s\n%!"     (Spawned.process_id ()) s
@@ -18,7 +18,7 @@ let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.p
 let stm_prerr_endline s = if !stm_debug then begin stm_pr_err (s ()) end else ()
 let stm_pperr_endline s = if !stm_debug then begin stm_pp_err (s ()) end else ()
 
-let stm_prerr_debug   s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
+let stm_prerr_debug   s = if CDebug.(get_flag misc) then begin stm_pr_err (s ()) end else ()
 
 open Pp
 open CErrors
@@ -785,7 +785,7 @@ end = struct (* {{{ *)
   end
 
   let print ?(now=false) () =
-    if !Flags.debug then NB.command ~now (print_dag !vcs)
+    if CDebug.(get_flag misc) then NB.command ~now (print_dag !vcs)
 
   let backup () = !vcs
   let restore v = vcs := v
@@ -1533,7 +1533,7 @@ end = struct (* {{{ *)
         when is_tac expr && Vernacstate.Stm.same_env o n -> (* A pure tactic *)
           Some (id, `ProofOnly (prev, Vernacstate.Stm.pstate n))
       | Some _, Some s ->
-        if !Flags.debug then msg_debug (Pp.str "STM: sending back a fat state");
+        if CDebug.(get_flag misc) then msg_debug (Pp.str "STM: sending back a fat state");
           Some (id, `Full s)
       | _, Some s -> Some (id, `Full s) in
     let rec aux seen = function
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index 56d88e6bd6..8be73ca028 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -22,14 +22,6 @@ let error_missing_arg s =
   exit 1
 
 (******************************************************************************)
-(* Imperative effects! This must be fixed at some point.                      *)
-(******************************************************************************)
-
-let set_debug () =
-  let () = Exninfo.record_backtrace true in
-  Flags.debug := true
-
-(******************************************************************************)
 
 type native_compiler = Coq_config.native_compiler =
   NativeOff | NativeOn of { ondemand : bool }
@@ -168,6 +160,9 @@ let add_load_vernacular opts verb s =
 let add_set_option opts opt_name value =
   { opts with pre = { opts.pre with injections = OptionInjection (opt_name, value) :: opts.pre.injections }}
 
+let add_set_debug opts flags =
+  add_set_option opts ["Debug"] (OptionAppend flags)
+
 (** Options for proof general *)
 let set_emacs opts =
   let opts = add_set_option opts Printer.print_goal_tag_opt_name (OptionSet None) in
@@ -382,10 +377,15 @@ let parse_args ~usage ~init arglist : t * string list =
     (* Options with zero arg *)
     |"-test-mode" -> Vernacinterp.test_mode := true; oval
     |"-beautify" -> Flags.beautify := true; oval
-    |"-bt" -> Exninfo.record_backtrace true; oval
+    |"-bt" -> add_set_debug oval "backtrace"
     |"-config"|"--config" -> set_query oval PrintConfig
-    |"-debug" -> set_debug (); oval
-    |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval
+
+    |"-debug" -> add_set_debug oval "all"
+    |"-d" | "-D" -> add_set_debug oval (next())
+
+    (* -xml-debug implies -debug. TODO don't be imperative here. *)
+    |"-xml-debug" -> Flags.xml_debug := true; add_set_debug oval "all"
+
     |"-diffs" ->
       add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ()))
     |"-emacs" -> set_emacs oval
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 6fb6cff04f..167f7d4026 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -562,19 +562,18 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   let open Context.Named.Declaration in
   let open ReductionBehaviour in
   let rec whrec cst_l (x, stack) =
-    let () = if debug_RAKAM () then
+    let () = debug_RAKAM (fun () ->
         let open Pp in
         let pr c = Termops.Internal.print_constr_env env sigma c in
-        Feedback.msg_debug
                (h (str "<<" ++ pr x ++
                    str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++
                    str "|" ++ cut () ++ Stack.pr pr stack ++
-                   str ">>"))
+                   str ">>")))
     in
     let c0 = EConstr.kind sigma x in
     let fold () =
-      let () = if debug_RAKAM () then
-          let open Pp in Feedback.msg_debug (str "<><><><><>") in
+      let () = debug_RAKAM (fun () ->
+          Pp.(str "<><><><><>")) in
       ((EConstr.of_kind c0, stack),cst_l)
     in
     match c0 with
diff --git a/test-suite/output/DebugFlags.out b/test-suite/output/DebugFlags.out
new file mode 100644
index 0000000000..0385413937
--- /dev/null
+++ b/test-suite/output/DebugFlags.out
@@ -0,0 +1,44 @@
+File "stdin", line 1, characters 0-16:
+Warning: There is no debug flag "cbn". [unknown-debug-flag,option]
+Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<?A -> ?A -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<?A -> ?A -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> nat|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> Prop|>>
+Debug: [RAKAM] <><><><><>
+Debug: [RAKAM] <<nat -> Prop|>>
+Debug: [RAKAM] <><><><><>
+2 + 3 = 0
+     : Prop
diff --git a/test-suite/output/DebugFlags.v b/test-suite/output/DebugFlags.v
new file mode 100644
index 0000000000..32c0f2d24b
--- /dev/null
+++ b/test-suite/output/DebugFlags.v
@@ -0,0 +1,5 @@
+Set Debug "cbn".
+
+Set Debug "RAKAM".
+
+Check 2 + 3 = 0.
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index bdb0cabacf..d859fcafe2 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -91,13 +91,14 @@ let remove_ids_and_lets env s ids =
 let record_proof_using expr =
   Aux_file.record_in_aux "suggest_proof_using" expr
 
+let debug_proof_using = CDebug.create ~name:"proof-using" ()
+
 (* Variables in [skip] come from after the definition, so don't count
    for "All". Used in the variable case since the env contains the
    variable itself. *)
 let suggest_common env ppid used ids_typ skip =
   let module S = Id.Set in
   let open Pp in
-  let print x = Feedback.msg_debug x in
   let pr_set parens s =
     let wrap ppcmds =
       if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
@@ -111,13 +112,13 @@ let suggest_common env ppid used ids_typ skip =
   in
   let all = S.diff all skip in
   let fwd_typ = close_fwd env (Evd.from_env env) ids_typ in
-  if !Flags.debug then begin
-    print (str "All "        ++ pr_set false all);
-    print (str "Type "       ++ pr_set false ids_typ);
-    print (str "needed "     ++ pr_set false needed);
-    print (str "all_needed " ++ pr_set false all_needed);
-    print (str "Type* "      ++ pr_set false fwd_typ);
-  end;
+  let () = debug_proof_using (fun () ->
+      str "All "        ++ pr_set false all ++ fnl() ++
+      str "Type "       ++ pr_set false ids_typ ++ fnl() ++
+      str "needed "     ++ pr_set false needed ++ fnl() ++
+      str "all_needed " ++ pr_set false all_needed ++ fnl() ++
+      str "Type* "      ++ pr_set false fwd_typ)
+  in
   let valid_exprs = ref [] in
   let valid e = valid_exprs := e :: !valid_exprs in
   if S.is_empty needed then valid (str "Type");
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 42ba63903d..c38cfbadc2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1645,6 +1645,13 @@ let () =
       optwrite = CWarnings.set_flags }
 
 let () =
+  declare_string_option
+    { optdepr  = false;
+      optkey   = ["Debug"];
+      optread  = CDebug.get_flags;
+      optwrite = CDebug.set_flags }
+
+let () =
   declare_bool_option
     { optdepr  = false;
       optkey   = ["Guard"; "Checking"];
@@ -1710,9 +1717,9 @@ let vernac_set_append_option ~locality key s =
 
 let vernac_set_option ~locality table v = match v with
 | OptionSetString s ->
-  (* We make a special case for warnings because appending is their
-  natural semantics *)
-  if CString.List.equal table ["Warnings"] then
+  (* We make a special case for warnings and debug flags because appending is
+  their natural semantics *)
+  if CString.List.equal table ["Warnings"] || CString.List.equal table ["Debug"] then
     vernac_set_append_option ~locality table s
   else
     let (last, prefix) = List.sep_last table in