diff options
| author | Théo Zimmermann | 2019-03-12 21:48:04 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-12 21:48:04 +0100 |
| commit | a249cc95c1345442c67e240e881fb653579ee386 (patch) | |
| tree | 9ac27e3b3964bcf2434148740ba2b32ab09c6c16 | |
| parent | f1d60cad76439d96da36ed7c52ff71b1b9573b80 (diff) | |
[refman] Add 'warn' option to coqtop directive.
Fix semantic conflict between #9389 and #9654.
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 8b7e5c9a02..b59d0bb723 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1655,7 +1655,7 @@ Declaring Implicit Arguments For instance in - .. coqtop:: all + .. coqtop:: all warn Arguments prod _ [_]. |