4 files changed, 22 insertions, 13 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 83e866e9f3..79060e6062 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -391,9 +391,11 @@ Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 \end{coq_example}
 
-\noindent If an inductive constructor or type has arity 2 and the corresponding 
-string is enclosed by parenthesis, then the rest of the string is used
-as infix constructor or type. 
+\noindent When extracting to {\ocaml}, if an inductive constructor or type
+has arity 2 and the corresponding string is enclosed by parentheses,
+and the string meets {\ocaml}'s lexical criteria for an infix symbol,
+then the rest of the string is used as infix constructor or type.
+
 \begin{coq_example}
 Extract Inductive list => "list" [ "[]" "(::)" ].
 Extract Inductive prod => "(*)"  [ "(,)" ].
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 8b1fc7c8f3..04a8a25c12 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -299,8 +299,9 @@ The following command-line options are recognized by the commands {\tt
 
 \section{Compiled libraries checker ({\tt coqchk})}
 
-The {\tt coqchk} command takes a list of library paths as argument.
-The corresponding compiled libraries (.vo files) are searched in the
+The {\tt coqchk} command takes a list of library paths as argument, described
+either by their logical name or by their physical filename, which must end in
+{\tt .vo}. The corresponding compiled libraries (.vo files) are searched in the
 path, recursively processing the libraries they depend on. The content
 of all these libraries is then type-checked. The effect of {\tt
   coqchk} is only to return with normal exit code in case of success,
@@ -330,9 +331,12 @@ code, it cannot be guaranteed that the produced compiled libraries are
 correct. {\tt coqchk} is a standalone verifier, and thus it cannot be
 tainted by such malicious code.
 
-Command-line options {\tt -I}, {\tt -R}, {\tt -where} and
+Command-line options {\tt -Q}, {\tt -R}, {\tt -where} and
 {\tt -impredicative-set} are supported by {\tt coqchk} and have the
-same meaning as for {\tt coqtop}. Extra options are:
+same meaning as for {\tt coqtop}. As there is no notion of relative paths in
+object files {\tt -Q} and {\tt -R} have exactly the same meaning.
+
+Extra options are:
 \begin{description}
 \item[{\tt -norec} {\em module}]\ %
 
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 5fb4585884..7034c56081 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -311,10 +311,11 @@ A sequence is an expression of the following form:
 \begin{quote}
 {\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$
 \end{quote}
-The expressions {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated
-to $v_1$ and $v_2$ which have to be tactic values. The tactic $v_1$ is
-then applied and $v_2$ is applied to the goals generated by the
-application of $v_1$. Sequence is left-associative.
+The expression {\tacexpr}$_1$ is evaluated to $v_1$, which must be
+a tactic value. The tactic $v_1$ is applied to the current goal,
+possibly producing more goals. Then {\tacexpr}$_2$ is evaluated to
+produce $v_2$, which must be a tactic value. The tactic $v_2$ is applied to
+all the goals produced by the prior application. Sequence is associative.
 
 \subsubsection[Local application of tactics]{Local application of tactics\tacindex{[>\ldots$\mid$\ldots$\mid$\ldots]}\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}\index{Tacticals![> \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}\index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}}
 %\tacindex{; [ | ]}
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 75fac9454a..a1a6a43918 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -285,8 +285,10 @@ universes and explicitly instantiate polymorphic definitions.
   \label{UniverseCmd}}
 
 In the monorphic case, this command declares a new global universe named
-{\ident}. It supports the polymorphic flag only in sections, meaning the
-universe quantification will be discharged on each section definition
+{\ident}, which can be referred to using its qualified name as
+well. Global universe names live in a separate namespace. The command
+supports the polymorphic flag only in sections, meaning the universe
+quantification will be discharged on each section definition
 independently. One cannot mix polymorphic and monomorphic declarations
 in the same section.