2 files changed, 7 insertions, 2 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 66a5f107a5..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
@@ -3611,7 +3611,7 @@ $\beta$-expansion (the inverse of $\bt$-reduction) of the current goal
 \item applying the abstracted goal to {\term}
 \end{enumerate}
 
-For instance, if the current goal $T$ is expressible has $\phi(t)$
+For instance, if the current goal $T$ is expressible as $\phi(t)$
 where the notation captures all the instances of $t$ in $\phi(t)$,
 then {\tt pattern $t$} transforms it into {\tt (fun x:$A$ => $\phi(${\tt
 x}$)$) $t$}.  This command can be used, for instance, when the tactic