From ed5d9cb136384ce0f7363a1c839ff0f9a7e9df7b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 26 Jun 2009 17:16:23 +0000
Subject: Add doc for [Print Opaque Dependencies] and a better explanation for
 the flags of manual implicit arguments.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12211 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-oth.tex | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index cc6c4c483c..630845d4ba 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -92,6 +92,13 @@ variables) a theorem or definition depends on.  Especially, it informs
 on the assumptions with respect to which the validity of a theorem
 relies.
 
+\begin{Variants}
+\item \texttt{\tt Print Opaque Dependencies {\qualid}.
+  \comindex{Print Opaque Dependencies}}\\
+  Displays the set of opaque constants {\qualid} relies on in addition
+  to the assumptions.
+\end{Variants}
+
 \subsection[\tt Search {\qualid}.]{\tt Search {\qualid}.\comindex{Search}}
 This command displays the name and type of all theorems of the current
 context whose statement's conclusion has the form {\tt ({\qualid} t1 ..
-- 
cgit v1.2.3