diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-04 16:26:37 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-04 16:26:37 +0100 |
| commit | 5003953d45ea0e780cd50bb9d6521799adf18079 (patch) | |
| tree | 6b784e05f1cc59f291c0cff39f6a94ff51837f4b /doc | |
| parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) | |
| parent | 893f8a3a3c573ab6b11cc3938cc67ccdc1b6b4ea (diff) | |
Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document supported scenarios.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 1cd23c929..bef31d3fa 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}} |