From 32a26cd2dde0f9c31fec6952c830eb09bfb260d8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 9 Jun 2008 11:26:32 +0000
Subject: - 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
---
 doc/refman/RefMan-mod.tex | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'doc/refman/RefMan-mod.tex')

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}
-- 
cgit v1.2.3