diff options
Diffstat (limited to 'doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst')
| -rw-r--r-- | doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst | 19 |
1 files changed, 19 insertions, 0 deletions
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`` |