From 20de2185c8b9887d0ad83fc7c2bb82ab6bfe39d6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 1 Apr 2015 19:00:54 +0200
Subject: Documenting "From * Require *" and clearing a bit the loadpath
 chapter.

---
 doc/refman/RefMan-oth.tex | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

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

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 556a2dab58..85deb31756 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -553,10 +553,11 @@ the form {\dirpath}{\tt .}{\textsl{ident}} and the file {\ident}{\tt
 mapped in {\Coq} loadpath to the logical path {\dirpath} (see
 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.
+with the mapping used to compile the file. If several files match, one of them
+is picked in an unspecified fashion.
 
 \begin{Variants}
-\item {\tt Require Import {\qualid}.} \comindex{Require} 
+\item {\tt Require Import {\qualid}.} \comindex{Require Import}
 
   This loads and declares the module {\qualid} and its dependencies
   then imports the contents of {\qualid} as described in
@@ -585,6 +586,15 @@ with the mapping used to compile the file.
   given, it also imports {\qualid}$_1$, \ldots, {\qualid}$_n$ and all
   the recursive dependencies that were marked or transitively marked
   as {\tt Export}.
+
+\item {\tt From {\dirpath} Require {\qualid}.}
+  \comindex{From Require}
+
+  This command acts as {\tt Require}, but picks any library whose absolute name
+  is of the form {\tt{\dirpath}.{\dirpath'}.{\qualid}} for some {\dirpath'}.
+  This is useful to ensure that the {\qualid} library comes from a given
+  package by expliciting its absolute root.
+
 \end{Variants}
 
 \begin{ErrMsgs}
-- 
cgit v1.2.3


From 226bf474155092f41cbb0d3e47143ac221947342 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 1 Apr 2015 21:32:38 +0200
Subject: Fixing a few typos + some uniformization of writing in doc.

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

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

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 85deb31756..4952ed7785 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -4,7 +4,7 @@
 \section{Displaying}
 
 \subsection[\tt Print {\qualid}.]{\tt Print {\qualid}.\comindex{Print}}
-This command displays on the screen informations about the declared or
+This command displays on the screen information about the declared or
 defined object referred by {\qualid}.
 
 \begin{ErrMsgs}
@@ -20,7 +20,7 @@ global constant.
 \item {\tt About {\qualid}.}
 \label{About}
 \comindex{About}\\ 
-This displays various informations about the object denoted by {\qualid}:
+This displays various information about the object denoted by {\qualid}:
 its kind (module, constant, assumption, inductive,
 constructor, abbreviation, \ldots), long name, type, implicit
 arguments and argument scopes. It does not print the body of
@@ -34,7 +34,7 @@ definitions or proofs.
 \end{Variants}
 
 \subsection[\tt Print All.]{\tt Print All.\comindex{Print All}}
-This command displays informations about the current state of the
+This command displays information about the current state of the
 environment, including sections and modules.
 
 \begin{Variants}
@@ -183,7 +183,7 @@ displayed as in \Coq\ terms.
 \begin{Variants}
 \item \texttt{Recursive Extraction} {\qualid$_1$} \ldots{} {\qualid$_n$}{\tt .}\\
   Recursively extracts all the material needed for the extraction of 
-  globals {\qualid$_1$}, \ldots, {\qualid$_n$}.
+  global {\qualid$_1$}, \ldots, {\qualid$_n$}.
 \end{Variants}
 
 \SeeAlso Chapter~\ref{Extraction}.
@@ -294,7 +294,7 @@ Search "+"%Z "*"%Z "distr" -positive -Prop.
 Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
 \end{coq_example}
 
-\Warning \comindex{SearchAbout} Up to Coq version 8.4, {\tt Search}
+\Warning \comindex{SearchAbout} Up to {\Coq} version 8.4, {\tt Search}
 had the behavior of current {\tt SearchHead} and the behavior of
 current {\tt Search} was obtained with command {\tt SearchAbout}. For
 compatibility, the deprecated name {\tt SearchAbout} can still be used
@@ -343,7 +343,7 @@ No module \module{} has been required (see Section~\ref{Require}).
 
 \end{Variants}
 
-\Warning Up to Coq version 8.4, {\tt SearchHead} was named {\tt Search}.
+\Warning Up to {\Coq} version 8.4, {\tt SearchHead} was named {\tt Search}.
 
 \subsection[\tt SearchPattern {\termpattern}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}}
 
@@ -458,8 +458,8 @@ The default blacklisted substrings are {\tt
 \label{Locate}}
 This command displays the full name of objects whose name is a prefix of the
 qualified identifier {\qualid}, and consequently the \Coq\ module in which they
-are defined. It searches for objects from the different qualified namespaces of
-Coq: terms, modules, Ltac, etc.
+are defined. It searches for objects from the different qualified name spaces of
+{\Coq}: terms, modules, Ltac, etc.
 
 \begin{coq_eval}
 (*************** The last line should produce **************************)
@@ -593,7 +593,7 @@ is picked in an unspecified fashion.
   This command acts as {\tt Require}, but picks any library whose absolute name
   is of the form {\tt{\dirpath}.{\dirpath'}.{\qualid}} for some {\dirpath'}.
   This is useful to ensure that the {\qualid} library comes from a given
-  package by expliciting its absolute root.
+  package by making explicit its absolute root.
 
 \end{Variants}
 
@@ -620,7 +620,7 @@ is picked in an unspecified fashion.
   \index{Bad-magic-number@{\tt Bad Magic Number}}
   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.
+  version of {\Coq}.
 
 \item \errindex{The file {\ident}.vo contains library {\dirpath} and not
   library {\dirpath'}}
@@ -657,7 +657,7 @@ searched into the current {\ocaml} loadpath (see the command {\tt
 Add ML Path} in the Section~\ref{loadpath}).  Loading of {\ocaml}
 files is only possible under the bytecode version of {\tt coqtop}
 (i.e. {\tt coqtop} called with options {\tt -byte}, see chapter 
-\ref{Addoc-coqc}), or when Coq has been compiled with a version of
+\ref{Addoc-coqc}), or when {\Coq} has been compiled with a version of
 {\ocaml} that supports native {\tt Dynlink} ($\ge$ 3.11).
 
 \begin{Variants}
@@ -668,7 +668,7 @@ files is only possible under the bytecode version of {\tt coqtop}
 
 \begin{ErrMsgs}
 \item \errindex{File not found on loadpath : \str}
-\item \errindex{Loading of ML object file forbidden in a native Coq}
+\item \errindex{Loading of ML object file forbidden in a native {\Coq}}
 \end{ErrMsgs}
 
 \subsection[\tt Print ML Modules.]{\tt Print ML Modules.\comindex{Print ML Modules}}
@@ -679,7 +679,7 @@ should use the command \texttt{Locate File} (see Section~\ref{Locate File})
 \section[Loadpath]{Loadpath}
 
 Loadpaths are preferably managed using {\Coq} command line options
-(see Section~\ref{loadpath}) but there remains vernacular commands to
+(see Section~\ref{loadpath}) but there remain vernacular commands to
 manage them.
 
 \subsection[\tt Pwd.]{\tt Pwd.\comindex{Pwd}\label{Pwd}}
@@ -696,7 +696,7 @@ 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 is equivament to the command line option {\tt -Q {\dirpath}
+This command is equivalent to the command line option {\tt -Q {\dirpath}
   {\str}}. It adds the physical directory {\str} to the current {\Coq}
 loadpath and maps it to the logical directory {\dirpath}.
 
@@ -778,11 +778,11 @@ over the name of a module or of an object inside a module.
 
 This commands undoes all the effects of the last vernacular
 command. Commands read from a vernacular file via a {\tt Load} are
-considered as a single command. Proof managment commands
+considered as a single command. Proof management commands
 are also handled by this command (see Chapter~\ref{Proof-handling}).
 For that, {\tt Back} may have to undo more than one command in order
-to reach a state where the proof managment information is available.
-For instance, when the last command is a {\tt Qed}, the managment
+to reach a state where the proof management information is available.
+For instance, when the last command is a {\tt Qed}, the management
 information about the closed proof has been discarded. In this case,
 {\tt Back} will then undo all the proof steps up to the statement of
 this proof.
@@ -803,7 +803,7 @@ this proof.
 \subsection[\tt BackTo $\num$.]{\tt BackTo $\num$.\comindex{BackTo}}
 \label{sec:statenums}
 
-This command brings back the system to the state labelled $\num$,
+This command brings back the system to the state labeled $\num$,
 forgetting the effect of all commands executed after this state.
 The state label is an integer which grows after each successful command.
 It is displayed in the prompt when in \texttt{-emacs} mode.
@@ -814,14 +814,14 @@ extra commands and end on a state $\num' \leq \num$ if necessary.
 \begin{Variants}
 \item {\tt Backtrack $\num_1$ $\num_2$ $\num_3$}.\comindex{Backtrack}\\
   {\tt Backtrack} is a \emph{deprecated} form of {\tt BackTo} which
-  allows explicitely manipulating the proof environment. The three
+  allows explicitly manipulating the proof environment. The three
   numbers $\num_1$, $\num_2$ and $\num_3$ represent the following:
 \begin{itemize}
 \item $\num_3$: Number of \texttt{Abort} to perform, i.e. the number
   of currently opened nested proofs that must be canceled (see
   Chapter~\ref{Proof-handling}).
 \item $\num_2$: \emph{Proof state number} to unbury once aborts have
-  been done. Coq will compute the number of \texttt{Undo} to perform
+  been done. {\Coq} will compute the number of \texttt{Undo} to perform
   (see Chapter~\ref{Proof-handling}).
 \item $\num_1$: State label to reach, as for {\tt BackTo}.
 \end{itemize}
@@ -949,7 +949,7 @@ algorithm that first normalizes the terms before comparing them.  The
 second algorithm is based on a bytecode representation of terms
 similar to the bytecode representation used in the ZINC virtual
 machine~\cite{Leroy90}. It is especially useful for intensive
-computation of algebraic values, such as numbers, and for reflexion-based
+computation of algebraic values, such as numbers, and for reflection-based
 tactics. The commands to fine-tune the reduction strategies and the
 lazy conversion algorithm are described first.
 
-- 
cgit v1.2.3

