- Documentation de admit et Print Assumptions.

- Relecture, mise à jour, correction d'erreurs et petite
  réorganisation du chapitre sur les commandes vernaculaires.
- Correction bug #1865 (rafraichissement des univers algébriques).
- Suppression de la dépendance du initial.coq en les noms longs des fichiers
  de façons à ce que les dépendances ne soient que purement logique.
- Encore un (petit) bug undo ide.	


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11077 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 0 deletions

diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index caa75d977c..12cfacbc49 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -355,6 +355,9 @@ Check T. (* Now correct *)
 Reset Mod.
 \end{coq_eval}
 
+Some features defined in modules are activated only when a module is
+imported. This is for instance the case of notations (see
+Section~\ref{Notation}).
 
 \begin{Variants}
 \item{\tt Export {\qualid}}\comindex{Export}