aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/proof-engine')
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 6fde52f95e..3ca0ffe678 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3554,6 +3554,7 @@ corresponding new goals will be generated.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
+ Set Warnings "-notation-overridden".
.. coqtop:: all