2 files changed, 4 insertions, 10 deletions
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 bfaf746a06..4f937ad727 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.
 
@@ -659,10 +657,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