From a249cc95c1345442c67e240e881fb653579ee386 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 12 Mar 2019 21:48:04 +0100
Subject: [refman] Add 'warn' option to coqtop directive.

Fix semantic conflict between #9389 and #9654.
---
 doc/sphinx/language/gallina-extensions.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 _ [_].
 
-- 
cgit v1.2.3