diff options
Diffstat (limited to 'doc/refman/RefMan-pro.tex')
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 52d8c09c1..c05fc829e 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -174,7 +174,7 @@ proof was edited. \subsection[\tt Existential {\num} := {\term}.]{\tt Existential {\num} := {\term}.\comindex{Existential} \label{Existential}} -This command allows to instantiate an existential variable. {\tt \num} +This command instantiates an existential variable. {\tt \num} is an index in the list of uninstantiated existential variables displayed by {\tt Show Existentials.} (described in Section~\ref{Show}) @@ -395,7 +395,7 @@ of interactive proof construction, the check of the termination (or guardedness) of the recursive calls in the fixpoint or cofixpoint constructions is postponed to the time of the completion of the proof. -The command \verb!Guarded! allows to verify if the guard condition for +The command \verb!Guarded! allows checking if the guard condition for fixpoint and cofixpoint is violated at some time of the construction of the proof without having to wait the completion of the proof." |