Skip to content
Browse files

Documenting the 'Printing Transparent/All Dependencies' command.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15946 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent 42a6fbf commit 1408c0f1ff3c25089c328d3d0a31144de0e718d0 @ppedrot ppedrot committed Oct 30, 2012
Showing with 7 additions and 0 deletions.
  1. +7 −0 doc/refman/RefMan-oth.tex
View
7 doc/refman/RefMan-oth.tex
@@ -155,6 +155,13 @@ \section{Requests to the environment}
\comindex{Print Opaque Dependencies}}\\
Displays the set of opaque constants {\qualid} relies on in addition
to the assumptions.
+\item \texttt{\tt Print Transparent Dependencies {\qualid}.
+ \comindex{Print Transparent Dependencies}}\\
+ Displays the set of transparent constants {\qualid} relies on in addition
+ to the assumptions.
+\item \texttt{\tt Print All Dependencies {\qualid}.
+ \comindex{Print All Dependencies}}\\
+ Displays all assumptions and constants {\qualid} relies on.
\end{Variants}
\subsection[\tt Search {\term}.]{\tt Search {\term}.\comindex{Search}}

0 comments on commit 1408c0f

Please sign in to comment.
Something went wrong with that request. Please try again.