[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.

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}}