diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 8 |
2 files changed, 13 insertions, 1 deletions
@@ -1,7 +1,11 @@ Changes from V8.3 to V8.4 ========================= -New proof engine +- New proof engine +- When the output file of "Print Universes" ends in ".dot" or ".gv", + the universe graph is printed in the DOT language, and can be + processed by Graphviz tools. + Changes from V8.2 to V8.3 ========================= diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 206607911b..7a56426c40 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1757,6 +1757,14 @@ The constraints on the internal level of the occurrences of {\Type} {\tt Print Universes.} \end{quote} +This command also accepts an optional output filename: +\begin{quote} +\tt Print Universes {\str}. +\end{quote} +If {\str} ends in \texttt{.dot} or \texttt{.gv}, the constraints are +printed in the DOT language, and can be processed by Graphviz +tools. The format is unspecified if {\str} doesn't end in +\texttt{.dot} or \texttt{.gv}. %%% Local Variables: %%% mode: latex |