aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-11 23:26:10 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-02-28 18:14:54 +0100
commitf5abd069a86b85829ab49141d27ef7633f4b84a1 (patch)
treef8855946b56d03188a6415e81cbf94cdde2ae0b2 /doc
parentf726e860917b56abc94f21d9d5add7594d23bb6d (diff)
[toplevel] [vernac] Remove Load hack and check supported scenarios.
Parsing in `VernacLoad` was broken for a while, but the situation has improved by miscellaneous refactoring. However, we still cannot support `Load` properly when proofs are crossing file boundaries. So in this patch we do two things: - We check for supported scenarios [no proofs open at `Load` entry/exit] - Remove the hack in `toplevel` so the behavior of `Load` is consistent between `coqide`/`coqc`. We close #5053 as its main bug was fixed by the main toplevel refactoring and the remaining cases are documented now.
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-oth.tex5
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}}