diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 7 |
2 files changed, 6 insertions, 4 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 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} |