Fix the syntax explaining the warning attribute

coq-community · Aug 13, 2024 · 14b112a · 14b112a
1 parent 5b7af75
commit 14b112a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/README.md b/README.md
@@ -198,8 +198,8 @@ To build all the examples in `src/`, run `make`.
 
 - You can use `Set Warnings "-deprecated-syntactic-definition"` to achieve the
   same effect as `-w -deprecated-syntactic-definition` from the command line,
-  but from within a Coq file. At least as of Coq 8.19 you can also use
-  `#[warning=-"-deprecated-syntactic-definition]` to disable the warning for one command.
+  but from within a Coq file. As of Coq 8.18 you can also use
+  `#[warning="-deprecated-syntactic-definition"]` to disable the warning for one command.
 
 ## Using Coq