[sphinx] Add warn option to coqtop directive.

By default Coq warnings are made fatal when building the manual.

If you want to show a command resulting in a warning, use the warn
option.

Preexisting warnings are either fixed or marked as expected.

2 files changed, 6 insertions, 3 deletions

diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index c1eab8a970..d1b95e6203 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -606,7 +606,10 @@ Finally, it gives the definition of the usual orderings ``le``,
   single: ge (term)
   single: gt (term)
 
-.. coqtop:: in
+.. This emits a notation already used warning but it won't be shown to
+   the user.
+
+.. coqtop:: in warn
 
   Inductive le (n:nat) : nat -> Prop :=
   | le_n : le n n
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 9ab3f905e6..9bd41d79b7 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1023,7 +1023,7 @@ Mutually defined inductive types
 
    .. coqtop:: in
 
-      Variables A B : Set.
+      Parameters A B : Set.
 
       Inductive tree : Set := node : A -> forest -> tree
 
@@ -1533,7 +1533,7 @@ the following attributes names are recognized:
 
 .. example::
 
-   .. coqtop:: all reset
+   .. coqtop:: all reset warn
 
         From Coq Require Program.
         #[program] Definition one : nat := S _.