From 356597ffc42b9298e27e0af2cfd05fe73f6d1383 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 Oct 2014 13:24:52 +0200
Subject: Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)

---
 doc/refman/RefMan-ext.tex | 22 +++++++---------------
 1 file changed, 7 insertions(+), 15 deletions(-)

(limited to 'doc/refman/RefMan-ext.tex')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index f71f99e763..51aba95707 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1268,6 +1268,13 @@ After the above declaration is issued, implicit arguments can just (and
 have to) be skipped in any expression involving an application of
 {\qualid}.
 
+Implicit arguments can be cleared with the following syntax:
+
+\begin{quote}
+{\tt Arguments {\qualid} : clear implicits
+\comindex{Arguments}}
+\end{quote}
+
 \begin{Variants}
 \item {\tt Global Arguments {\qualid} \nelist{\possiblybracketedident}{}
 \comindex{Global Arguments}}
@@ -1403,21 +1410,6 @@ Variables (a b c : X) (r1 : R a b) (r2 : R b c).
 Check (p r1 r2).
 \end{coq_example}
 
-Implicit arguments can be cleared with the following syntax:
-
-\begin{quote}
-{\tt Arguments {\qualid} : clear implicits
-\comindex{Arguments}}
-\end{quote}
-
-In the following example implict arguments declarations for the {\tt nil}
-constant are cleared:
-\begin{coq_example}
-Arguments cons : clear implicits.
-Print Implicit cons.
-\end{coq_example}
-
-
 \subsection{Mode for automatic declaration of implicit arguments
 \label{Auto-implicit}
 \comindex{Set Implicit Arguments}
-- 
cgit v1.2.3

