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(-)

(limited to 'doc/refman')

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


From ca63912f21d0e88d3f4d1a37cc75f091b90bb077 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 22 Jul 2015 17:40:22 +0200
Subject: Refman: document Show Universes.

---
 doc/refman/RefMan-pro.tex | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 684a4add4c..7af87a399a 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -453,11 +453,16 @@ In the case of a non-product goal, it prints nothing.
 This command is similar to the previous one, it simulates the naming 
 process of an {\tt Intros}.
 
-\item{\tt Show Existentials\label{ShowExistentials}}\comindex{Show Existentials}
+\item{\tt Show Existentials.\label{ShowExistentials}}\comindex{Show Existentials}
 \\ It displays
 the set of all uninstantiated existential variables in the current proof tree, 
 along with the type and the context of each variable.
 
+\item{\tt Show Universes.\label{ShowUniverses}}\comindex{Show Universes}
+\\ It displays the set of all universe constraints and its
+normalized form at the current stage of the proof, useful for
+debugging universe inconsistencies.
+
 \end{Variants}
 
 
-- 
cgit v1.2.3