4 files changed, 22 insertions, 10 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 22c75b4fc8..cab6739998 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -462,11 +462,18 @@ abbreviate a type, like {\tt relation A := A -> A -> Prop}.
 
 This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_instances}.
 
+\subsection{\tt Set Typeclasses Axioms Are Instances}
+\optindex{Typeclasses Axioms Are Instances}
+
+This option (off by default since 8.8) automatically declares axioms
+whose type is a typeclass at declaration time as instances of that
+class.
+
 \subsection{\tt Set Typeclasses Dependency Order}
 \optindex{Typeclasses Dependency Order}
 
 This option (on by default since 8.6) respects the dependency order between
-subgoals, meaning that subgoals which are depended on by other subgoals 
+subgoals, meaning that subgoals which are depended on by other subgoals
 come first, while the non-dependent subgoals were put before the
 dependent ones previously (Coq v8.5 and below). This can result in quite
 different performance behaviors of proof search.
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-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.