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

2 files changed, 15 insertions, 8 deletions

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