aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-mod.tex
diff options
context:
space:
mode:
authorherbelin2008-06-29 16:24:36 +0000
committerherbelin2008-06-29 16:24:36 +0000
commit6735186e6458fedd57efd663c900166af0d6fce3 (patch)
tree7a4086e49840465ba00bca8569e4dd67554272a7 /doc/refman/RefMan-mod.tex
parent2040379ec1d79ff588498ca6f20d8c7b75d74533 (diff)
Lissage de la gestion des chemins de chargement de fichiers :
- Option -R fait maintenant des Import à tous les niveaux de la hiérarchie de répertoires. Par exemple, Require "Init.Wf" marche. - Option -I rend maintenant possible l'accès aux sous-répertoires via les noms qualifiés. Ainsi -R est exactement comme -I sauf qu'il rend récursivement visibles les noms non qualifiés. - Ajout option -I dir -as coqdir, et par symétrie, -R dir -as coqdir. - Ajout option -exclude-dir pour exclure certains sous-répertoires de la descente récursive de -R. - Amélioration message de localisation pour fichiers venant d'un "state". - Adaptation du checker (et ajout du test check_coq_overwriting qui semblait involontairement oublié dans l'option -R). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11188 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman/RefMan-mod.tex')
-rw-r--r--doc/refman/RefMan-mod.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index 12cfacbc49..2891ba2e9e 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -386,7 +386,7 @@ Prints the module type and (optionally) the body of the module {\ident}.
Prints the module type corresponding to {\ident}.
-\subsection{\texttt{Locate Module {\qualid}}
+\subsection{\tt Locate Module {\qualid}
\comindex{Locate Module}}
Prints the full name of the module {\qualid}.