From 246a5011d7a794835aa0f9ca198b3a4a74031ed6 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 22 Jul 2015 07:30:50 +0200
Subject: Remove obsolete documentation. (Fix bug #4238)

---
 doc/refman/RefMan-ext.tex | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index cc5239a779..d63d22a71c 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1375,9 +1375,6 @@ Check (fun l => map length l = map (list nat) nat length l).
 \Rem To know which are the implicit arguments of an object, use the command
 {\tt Print Implicit} (see \ref{PrintImplicit}).
 
-\Rem If the list of arguments is empty, the command removes the
-implicit arguments of {\qualid}.
-
 \subsection{Automatic declaration of implicit arguments for a constant}
 
 {\Coq} can also automatically detect what are the implicit arguments
-- 
cgit v1.2.3