From bb22f188b46527fb5829562edc946b743b326309 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Tue, 7 Jan 2020 11:34:31 +0100
Subject: Trailing implicit error: documentation

---
 doc/sphinx/language/gallina-extensions.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 78428be18f..6be501199d 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1728,11 +1728,11 @@ Declaring Implicit Arguments
    To know which are the implicit arguments of an object, use the
    command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`).
 
-.. warn:: Argument number @num is a trailing implicit so must be maximal.
+.. exn:: Argument id is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ].
 
    For instance in
 
-   .. coqtop:: all warn
+   .. coqtop:: all fail
 
       Arguments prod _ [_].
 
-- 
cgit v1.2.3