diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 5 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 |
2 files changed, 6 insertions, 1 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 1cd23c9297..bef31d3fa5 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -513,6 +513,9 @@ This command loads the file named {\ident}{\tt .v}, searching successively in each of the directories specified in the {\em loadpath}. (see Section~\ref{loadpath}) +Files loaded this way cannot leave proofs open, and neither the {\tt + Load} command can be use inside a proof. + \begin{Variants} \item {\tt Load {\str}.}\label{Load-str}\\ Loads the file denoted by the string {\str}, where {\str} is any @@ -530,6 +533,8 @@ successively in each of the directories specified in the {\em \begin{ErrMsgs} \item \errindex{Can't find file {\ident} on loadpath} +\item \errindex{Load is not supported inside proofs} +\item \errindex{Files processed by Load cannot leave open proofs} \end{ErrMsgs} \section[Compiled files]{Compiled files\label{compiled}\index{Compiled files}} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 9635b3ab1a..6dca314b4a 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2904,7 +2904,7 @@ This happens if \term$_1$ does not occur in the goal. rewrite H in H2 at - 2}. In particular a failure will happen if any of these three simpler tactics fails. \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in - H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen + H$_i$} for all hypotheses \texttt{H$_i$} different from \texttt{H}. A success will happen as soon as at least one of these simpler tactics succeeds. \item \texttt{rewrite H in *} is a combination of \texttt{rewrite H} and \texttt{rewrite H in * |-} that succeeds if at |