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

5 files changed, 146 insertions, 117 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index f74ace29f5..1bd3d148e2 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -84,7 +84,8 @@ only for developers that are writing their own tactics and are using
 you move the \Coq\ binaries and library after installation.
 
 \section[Options]{Options\index{Options of the command line}
-\label{vmoption}}
+\label{vmoption}
+\label{coqoptions}}
 
 The following command-line options are recognized by the commands {\tt
   coqc} and {\tt coqtop}, unless stated otherwise:
@@ -100,20 +101,48 @@ The following command-line options are recognized by the commands {\tt
 
 \item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ 
 
-  Add {\em directory} to the searched directories when looking for a
-  file.
+  Add physical path {\em directory} to the list of directories where to
+  look for a file and bind it to the empty logical directory. The
+  subdirectory structure of {\em directory} is recursively available
+  from {\Coq} using absolute names (see Section~\ref{LongNames}).
 
-\item[{\tt -R} {\em directory} {\dirpath}]\ 
+\item[{\tt -I} {\em directory} {\tt -as} {\em dirpath}]\ 
 
-  This maps the subdirectory structure of physical {\em directory} to
-  logical {\dirpath} and adds {\em directory} and its subdirectories
-  to the searched directories when looking for a file.
+  Add physical path {\em directory} to the list of directories where to
+  look for a file and bind it to the logical directory {\dirpath}.  The
+  subdirectory structure of {\em directory} is recursively available
+  from {\Coq} using absolute names extending the {\dirpath} prefix.
+
+  \SeeAlso {\tt Add LoadPath} in Section~\ref{AddLoadPath} and logical
+  paths in Section~\ref{Libraries}.
+
+\item[{\tt -R} {\em directory} {\dirpath}, {\tt -R} {\em directory} {\tt -as} {\dirpath}]\
+
+  Do as {\tt -I} {\em directory} {\tt -as} {\dirpath} but make the
+  subdirectory structure of {\em directory} recursively visible so
+  that the recursive contents of physical {\em directory} is available
+  from {\Coq} using short or partially qualified names.
+  
+  \SeeAlso {\tt Add Rec LoadPath} in Section~\ref{AddRecLoadPath} and logical
+  paths in Section~\ref{Libraries}.
 
 \item[{\tt -top} {\dirpath}]\ 
 
   This sets the toplevel module name to {\dirpath} instead of {\tt
   Top}. Not valid for {\tt coqc}.
 
+\item[{\tt -notop} {\dirpath}]\ 
+
+  This sets the toplevel module name to the empty logical dirpath. Not
+  valid for {\tt coqc}.
+
+\item[{\tt -exclude-dir} {\em subdirectory}]\ 
+
+  This tells to exclude any subdirectory named {\em subdirectory}
+  while processing option {\tt -R}. Without this option only the
+  conventional version control management subdirectories named {\tt
+  CVS} and {\tt \_darcs} are excluded.
+
 \item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}]\ 
 
   Cause \Coq~to use the state put in the file {\em file} as its input
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 5baf84becd..1294ee7c0b 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -851,106 +851,87 @@ section is closed.
 \subsection{Names of libraries and files
 \label{Libraries}
 \index{Libraries}
+\index{Physical paths}
 \index{Logical paths}}
 
 \paragraph{Libraries}
 
-The theories developed in {\Coq} are stored in {\em libraries}.  A
-library is characterized by a name called {\it root} of the
-library. The standard library of {\Coq} has root name {\tt Coq} and is
-known by default when a {\Coq} session starts.
-
-Libraries have a tree structure. E.g., the {\tt Coq} library
-contains the sub-libraries {\tt Init}, {\tt Logic}, {\tt Arith}, {\tt
-Lists}, ... The ``dot notation'' is used to separate the different
-component of a library name. For instance, the {\tt Arith} library of
-{\Coq} standard library is written ``{\tt Coq.Arith}''.
-
-\medskip
-\Rem no blank is allowed between the dot and the identifier on its
-right, otherwise the dot is interpreted as the full stop (period) of
-the command!
-\medskip
-
-\paragraph{Physical paths vs logical paths}
-
-Libraries and sub-libraries are denoted by {\em logical directory
-paths} (written {\dirpath} and of which the syntax is the same as
-{\qualid}, see \ref{qualid}). Logical directory
-paths can be mapped to physical directories of the
-operating system using the command (see \ref{AddLoadPath})
-\begin{quote}
-{\tt Add LoadPath {\it physical\_path} as {\dirpath}}.
-\end{quote}
-A library can inherit the tree structure of a physical directory by
-using the {\tt -R} option to {\tt coqtop} or the
-command (see \ref{AddRecLoadPath})
-\begin{quote}
-{\tt Add Rec LoadPath {\it physical\_path} as {\dirpath}}.
-\end{quote}
-
-\Rem When used interactively with {\tt coqtop} command, {\Coq} opens a
-library called {\tt Top}.
-
-\paragraph{The file level}
-
-At some point, (sub-)libraries contain {\it modules} which coincide
-with files at the physical level.  As for sublibraries, the dot
-notation is used to denote a specific module of a library. Typically,
-{\tt Coq.Init.Logic} is the logical path associated to the file {\tt
-  Logic.v} of {\Coq} standard library.  Notice that compilation (see
-\ref{Addoc-coqc}) is done at the level of files.
-
-If the physical directory where a file {\tt File.v} lies is mapped to
-the empty logical directory path (which is the default when using the
-simple form of {\tt Add LoadPath} or {\tt -I} option to coqtop), then
-the name of the module it defines is {\tt File}.
+The theories developed in {\Coq} are stored in {\em library files}
+which are hierarchically classified into {\em libraries} and {\em
+sublibraries}. To express this hierarchy, library names are
+represented by qualified identifiers {\qualid}, i.e. as list of
+identifiers separated by dots (see Section~\ref{qualid}). For
+instance, the library file {\tt Mult} of the standard {\Coq} library
+{\tt Arith} has name {\tt Coq.Arith.Mult}. The identifier
+that starts the name of a library is called a {\em library root}.
+All library files of the standard library of {\Coq} have reserved root
+{\tt Coq} but library file names based on other roots can be obtained
+by using {\tt coqc} options {\tt -I} or {\tt -R} (see
+Section~\ref{coqoptions}). Also, when an interactive {\Coq} session
+starts, a library of root {\tt Top} is started, unless option {\tt
+-top} or {\tt -notop} is set (see Section~\ref{coqoptions}).
+
+As library files are stored on the file system of the underlying
+operating system, a translation from file-system names to {\Coq} names
+is needed. In this translation, names in the file system are called
+{\em physical} paths while {\Coq} names are contrastingly called {\em
+logical} names. Logical names are mapped to physical paths using the
+commands {\tt Add LoadPath} or {\tt Add Rec LoadPath} (see
+Sections~\ref{AddLoadPath} and~\ref{AddRecLoadPath}).
 
 \subsection{Qualified names
 \label{LongNames}
 \index{Qualified identifiers}
 \index{Absolute names}}
 
-Modules contain constructions (sub-modules, axioms, parameters,
-definitions, lemmas, theorems, remarks or facts). The (full) name of a
-construction starts with the logical name of the module in which it is defined
-followed by the (short) name of the construction.
-Typically, the full name {\tt Coq.Init.Logic.eq} denotes Leibniz' equality
-defined in the module {\tt Logic} in the sublibrary {\tt Init} of the
-standard library of \Coq.
-
-\paragraph{Absolute, partially qualified and short names}
-
-The full name of a library, module, section, definition, theorem,
-... is its {\it absolute name}.  The last identifier ({\tt eq} in the
-previous example) is its {\it short name} (or sometimes {\it base
-name}). Any suffix of the absolute name is a {\em partially qualified
-name} (e.g. {\tt Logic.eq} is a partially qualified name for {\tt
-Coq.Init.Logic.eq}). Partially qualified names (shortly {\em
-qualified name}) are also built from identifiers separated by dots.
-They are written {\qualid} in the documentation.
+Library files are modules which possibly contain submodules which
+eventually contain constructions (axioms, parameters, definitions,
+lemmas, theorems, remarks or facts). The {\em absolute name}, or {\em
+full name}, of a construction in some library file is a qualified
+identifier starting with the logical name of the library file,
+followed by the sequence of submodules names encapsulating the
+construction and ended by the proper name of the construction.
+Typically, the absolute name {\tt Coq.Init.Logic.eq} denotes Leibniz'
+equality defined in the module {\tt Logic} in the sublibrary {\tt
+Init} of the standard library of \Coq.
+
+The proper name that ends the name of a construction is the {\it short
+name} (or sometimes {\it base name}) of the construction (for
+instance, the short name of {\tt Coq.Init.Logic.eq} is {\tt eq}). Any
+partial suffix of the absolute name is a {\em partially qualified name}
+(e.g. {\tt Logic.eq} is a partially qualified name for {\tt
+Coq.Init.Logic.eq}).  Especially, the short name of a construction is
+its shortest partially qualified name.
 
 {\Coq} does not accept two constructions (definition, theorem, ...)
 with the same absolute name but different constructions can have the
 same short name (or even same partially qualified names as soon as the
 full names are different).
 
-\paragraph{Visibility}
+Notice that the notion of absolute, partially qualified and
+short names also applies to library file names.
 
-{\Coq} maintains a {\it name table} mapping qualified names to absolute
-names. This table is modified by the commands {\tt Require} (see
-\ref{Require}), {\tt Import} and {\tt Export} (see \ref{Import}) and
-also each time a new declaration is added to the context.
+\paragraph{Visibility}
 
-An absolute name is called {\it visible} from a given short or
-partially qualified name when this name suffices to denote it. This
-means that the short or partially qualified name is mapped to the absolute
-name in {\Coq} name table.
+{\Coq} maintains a table called {\it name table} which maps partially
+qualified names of constructions to absolute names. This table is
+updated by the commands {\tt Require} (see \ref{Require}), {\tt
+Import} and {\tt Export} (see \ref{Import}) and also each time a new
+declaration is added to the context. An absolute name is called {\it
+visible} from a given short or partially qualified name when this
+latter name is enough to denote it. This means that the short or
+partially qualified name is mapped to the absolute name in {\Coq} name
+table.
+
+A similar table exists for library file names. It is updated by the
+vernacular commands {\tt Add LoadPath} and {\tt Add Rec LoadPath} (or
+their equivalent as options of the {\Coq} executables, {\tt -I} and
+{\tt -R}).
 
 It may happen that a visible name is hidden by the short name or a
 qualified name of another construction. In this case, the name that
 has been hidden must be referred to using one more level of
-qualification. Still, to ensure that a construction always remains
+qualification. To ensure that a construction always remains
 accessible, absolute names can never be hidden.
 
 Examples:
@@ -965,14 +946,8 @@ Check Datatypes.nat.
 Locate nat.
 \end{coq_example}
 
-\Rem There is also a name table for sublibraries, modules and sections.
-
-\Rem In versions prior to {\Coq} 7.4, lemmas declared with {\tt
-Remark} and {\tt Fact} kept in their full name the names of the
-sections in which they were defined. Since {\Coq} 7.4, they strictly
-behaves as {\tt Theorem} and {\tt Lemma} do.
-
-\SeeAlso Command {\tt Locate} in Section~\ref{Locate}.
+\SeeAlso Command {\tt Locate} in Section~\ref{Locate} and {\tt Locate
+Library} in Section~\ref{Locate Library}.
 
 %% \paragraph{The special case of remarks and facts}
 %% 
@@ -985,16 +960,6 @@ behaves as {\tt Theorem} and {\tt Lemma} do.
 %% a fact {\tt F} is defined in subsection {\tt S2} of section {\tt S1}
 %% in module {\tt M}, then its absolute name is {\tt M.S1.F}.
 
-
-\paragraph{Requiring a file}
-
-A module compiled in a ``.vo'' file comes with a logical names (e.g. 
-physical file \verb!theories/Init/Datatypes.vo! in the {\Coq} installation directory is bound to the logical module {\tt Coq.Init.Datatypes}). 
-When requiring the file, the mapping between physical directories and logical library should be consistent with the mapping used to compile the file (for modules of the standard library, this is automatic -- check it by typing {\tt Print LoadPath}).
-
-The command {\tt Add Rec LoadPath} is also available from {\tt coqtop}
-and {\tt coqc} by using option~\verb=-R=.
-
 \section{Implicit arguments
 \index{Implicit arguments}
 \label{Implicit Arguments}}
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}.
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 76faac5935..ec07dc079c 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -427,12 +427,14 @@ replayed nor rechecked.
 
 To locate the file in the file system, {\qualid} is decomposed under
 the form {\dirpath}{\tt .}{\textsl{ident}} and the file {\ident}{\tt
-.vo} is searched in the directory of the physical file system that is
+.vo} is searched in the physical directory of the file system that is
 mapped in {\Coq} loadpath to the logical path {\dirpath} (see
-Section~\ref{Loadpath}).
+Section~\ref{loadpath}). The mapping between physical directories and
+logical names at the time of requiring the file must be consistent
+with the mapping used to compile the file.
 
 \begin{Variants}
-\item {\tt Require Import {\qualid}.}\\ \comindex{Require} 
+\item {\tt Require Import {\qualid}.} \comindex{Require} 
 
   This loads and declares the module {\qualid} and its dependencies
   then imports the contents of {\qualid} as described in
@@ -493,6 +495,15 @@ Section~\ref{Loadpath}).
   The file {\tt{\ident}.vo} was found but either it is not a \Coq\
   compiled module, or it was compiled with an older and incompatible
   version of \Coq.
+
+\item \errindex{The file {\ident}.vo contains library {\dirpath} and not
+  library {\dirpath'}}
+
+  The library file {\dirpath'} is indirectly required by the {\tt
+  Require} command but it is bound in the current loadpath to the file
+  {\ident}.vo which was bound to a different library name {\dirpath}
+  at the time it was compiled.
+
 \end{ErrMsgs}
 
 \SeeAlso Chapter~\ref{Addoc-coqc}
@@ -546,10 +557,13 @@ which can be any valid path.
 
 \subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}}
 
-This command adds the path {\str} to the current {\Coq} loadpath and
-maps it to the logical directory {\dirpath}, which means that every
-file {\tt M.v} physically lying in directory {\str} becomes accessible
-through logical name ``{\dirpath}{\tt{.M}}''. 
+This command adds the physical directory {\str} to the current {\Coq}
+loadpath and maps it to the logical directory {\dirpath}, which means
+that every file \textrm{\textsl{dirname}}/\textrm{\textsl{basename.v}}
+physically lying in subdirectory {\str}/\textrm{\textsl{dirname}}
+becomes accessible in {\Coq} through absolute logical name
+{\dirpath}{\tt .}\textrm{\textsl{dirname}}{\tt
+.}\textrm{\textsl{basename}}.
 
 \Rem {\tt Add LoadPath} also adds {\str} to the current ML loadpath.
 
@@ -559,8 +573,27 @@ Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory
 \end{Variants}
 
 \subsection[\tt Add Rec LoadPath {\str} as {\dirpath}.]{\tt Add Rec LoadPath {\str} as {\dirpath}.\comindex{Add Rec LoadPath}\label{AddRecLoadPath}}
-This command adds the directory {\str} and all its subdirectories 
-to the current \Coq\ loadpath. The top directory {\str} is mapped to the logical directory {\dirpath} while any subdirectory {\textsl{pdir}} is mapped to logical directory {\dirpath}{\tt{.pdir}} and so on.
+This command adds the physical directory {\str} and all its subdirectories to
+the current \Coq\ loadpath. The top directory {\str} is mapped to the
+logical directory {\dirpath} and any subdirectory {\textsl{pdir}} of it is
+mapped to logical name {\dirpath}{\tt .}\textsl{pdir} and
+recursively. Subdirectories corresponding to invalid {\Coq}
+identifiers are skipped, and, by convention, subdirectories named {\tt
+CVS} or {\tt \_darcs} are skipped too.
+
+Otherwise, said, {\tt Add Rec LoadPath {\str} as {\dirpath}} behaves
+as {\tt Add LoadPath {\str} as {\dirpath}} excepts that files lying in
+validly named subdirectories of {\str} need not be qualified to be
+found.
+
+In case of files with identical base name, files lying in most recently
+declared {\dirpath} are found first and explicit qualification is
+required to refer to the other files of same base name.
+
+If several files with identical base name are present in different
+subdirectories of a recursive loadpath declared via a single instance of
+{\tt Add Rec LoadPath}, which of these files is found first is
+system-dependent and explicit qualification is recommended.
 
 \Rem {\tt Add Rec LoadPath} also recursively adds {\str} to the current ML loadpath.
 
@@ -600,7 +633,7 @@ command {\tt Declare ML Module} in the section
 This command displays the location of file {\str} in the current loadpath.
 Typically, {\str} is a \texttt{.cmo} or \texttt{.vo} or \texttt{.v} file.
 
-\subsection[\tt Locate Library {\dirpath}.]{\tt Locate Library {\dirpath}.\comindex{Locate Library}}
+\subsection[\tt Locate Library {\dirpath}.]{\tt Locate Library {\dirpath}.\comindex{Locate Library}\label{Locate Library}}
 This command gives the status of the \Coq\ module {\dirpath}. It tells if the
 module is loaded and if not searches in the load path for a module
 of logical name {\dirpath}.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 8539136a0a..9f6fa8be14 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1543,7 +1543,7 @@ induction n.
   This syntax is used for selecting which occurrences of {\term} the
   induction has to be carried on. The {\tt in {\atoccurrences}} clause is an
   occurrence clause whose syntax and behavior is described in
-  Section~\ref{Occurrences clause}.
+  Section~\ref{Occurrences clauses}.
 
   When an occurrence clause is given, an equation between {\term} and
   the value it gets in each case of the induction is added to the
@@ -2448,8 +2448,10 @@ the given bindings to instantiate parameters or hypotheses of {\term}.
 
 \item \texttt{discriminate}
 
-  This looks for a quantified or not quantified hypothesis {\ident} on
-  which {\tt discriminate {\ident}} is applicable.
+  This behaves like {\tt discriminate {\ident}} if {\ident} is the
+  name of an hypothesis to which {\tt discriminate} is applicable; if
+  the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$},
+  this behaves as {\tt intro {\ident}; injection {\ident}}.
 
   \begin{ErrMsgs}
   \item \errindex{No discriminable equalities} \\