From dca4b978ff8bfa2eeee864edac4199d9d9df3d5e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 25 Dec 2014 22:31:34 +0100
Subject: Document 6d5b56d971 (forbid Require inside modules).

---
 doc/refman/RefMan-oth.tex | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index e4c83a59c3..64fab055ea 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -702,6 +702,13 @@ with the mapping used to compile the file.
   {\ident}.vo which was bound to a different library name {\dirpath}
   at the time it was compiled.
 
+\item \errindex{Require is not allowed inside a module or a module type}
+
+  This command is not allowed inside a module or a module type being defined.
+  It is meant to describe a dependency between compilation units. Note however
+  that the commands {\tt Import} and {\tt Export} alone can be used inside
+  modules (see Section~\ref{Import}).
+
 \end{ErrMsgs}
 
 \SeeAlso Chapter~\ref{Addoc-coqc}
-- 
cgit v1.2.3