Merge branch 'v8.5'

6 files changed, 23 insertions, 23 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 3605a716e7..1eb40cd36d 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1782,14 +1782,14 @@ This is useful for declaring the implicit type of a single variable.
 Implicit generalization is an automatic elaboration of a statement with
 free variables into a closed statement where these variables are
 quantified explicitly. Implicit generalization is done inside binders
-starting with a \verb|`| and terms delimited by \verb|`{ }| and
-\verb|`( )|, always introducing maximally inserted implicit arguments for
+starting with a \texttt{\`{}} and terms delimited by \texttt{\`{}\{ \}} and
+\texttt{\`{}( )}, always introducing maximally inserted implicit arguments for
 the generalized variables. Inside implicit generalization
 delimiters, free variables in the current context are automatically
 quantified using a product or a lambda abstraction to generate a closed
 term. In the following statement for example, the variables \texttt{n}
 and \texttt{m} are automatically generalized and become explicit
-arguments of the lemma as we are using \verb|`( )|:
+arguments of the lemma as we are using \texttt{\`{}( )}:
 
 \begin{coq_example}
 Generalizable All Variables.
@@ -1834,7 +1834,7 @@ Definition id `(x : A) : A := x.
 Print id.
 \end{coq_example}
 
-The generalizing binders \verb|`{ }| and \verb|`( )| work similarly to
+The generalizing binders \texttt{\`{}\{ \}} and \texttt{\`{}( )} work similarly to
 their explicit counterparts, only binding the generalized variables
 implicitly, as maximally-inserted arguments. In these binders, the
 binding name for the bound object is optional, whereas the type is
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index ce230a0f73..40e0ecc11c 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -308,9 +308,9 @@ statement's conclusion has the form {\tt ({\term} t1 ..
   tn)}.  This command is useful to remind the user of the name of
 library lemmas.
 
-\begin{coq_example*}
+\begin{coq_eval}
 Reset Initial.
-\end{coq_example*}
+\end{coq_eval}
 
 \begin{coq_example}
 SearchHead le.
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 11954ed0ea..24417bd039 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -120,7 +120,7 @@ is on Figure~\ref{init-notations}.
 
 \subsection{Complex notations}
 
-Notations can be made from arbitraly complex symbols. One can for
+Notations can be made from arbitrarily complex symbols. One can for
 instance define prefix notations.
 
 \begin{coq_example*}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index dcc2bcc1f6..ee40a0d51e 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -906,7 +906,7 @@ containing {\tt *} or {\tt **}, {\tt intros $p_1$ ... $p_n$}
   variables or hypotheses until the goal is not any more a
   quantification or an implication;
 \item introduction over an introduction pattern $p$ introduces the
-  forthcoming quantified variables or premisse of the goal and applies
+  forthcoming quantified variables or premise of the goal and applies
   the introduction pattern $p$ to it.
 \end{itemize}
 
@@ -1020,13 +1020,13 @@ dependencies. This tactic is the inverse of {\tt intro}.
 This moves the hypothesis named {\ident$_1$} in the local context
 after the hypothesis named {\ident$_2$}. The proof term is not changed.
 
-If {\ident$_1$} comes before {\ident$_2$} in the order of dependences,
-then all hypotheses between {\ident$_1$} and {\ident$_2$} that
-(possibly indirectly) depend on {\ident$_1$} are moved also.
+If {\ident$_1$} comes before {\ident$_2$} in the order of dependencies,
+then all the hypotheses between {\ident$_1$} and {\ident$_2$} that
+(possibly indirectly) depend on {\ident$_1$} are moved too.
 
-If {\ident$_1$} comes after {\ident$_2$} in the order of dependences,
-then all hypotheses between {\ident$_1$} and {\ident$_2$} that
-(possibly indirectly) occur in {\ident$_1$} are moved also.
+If {\ident$_1$} comes after {\ident$_2$} in the order of dependencies,
+then all the hypotheses between {\ident$_1$} and {\ident$_2$} that
+(possibly indirectly) occur in {\ident$_1$} are moved too.
 
 \begin{Variants}
 
@@ -1339,7 +1339,7 @@ in the list of subgoals remaining to prove.
 \label{generalize}
 
 This tactic applies to any goal. It generalizes the conclusion with
-respect to one of its subterms.
+respect to some term.
 
 \Example
 
@@ -1415,7 +1415,7 @@ the number of the existential variable since this number is different
 in every session.
 
 When you are referring to hypotheses which you did not name
-explicitely, be aware that Coq may make a different decision on how to
+explicitly, be aware that Coq may make a different decision on how to
 name the variable in the current goal and in the context of the
 existential variable. This can lead to surprising behaviors.
 
@@ -1445,7 +1445,7 @@ a hypothesis or in the body or the type of a local definition.
 \label{admit}
 
 The {\tt admit} tactic ``solves'' the current subgoal by an
-axiom. This typically allows temporarily skiping a subgoal so as to
+axiom. This typically allows temporarily skipping a subgoal so as to
 progress further in the rest of the proof. To know if some proof still
 relies on unproved subgoals, one can use the command {\tt Print
 Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals
@@ -2744,7 +2744,7 @@ the same variants as {\tt rewrite} has.
 This tactic applies to any goal. It replaces all free occurrences of
 {\term$_1$} in the current goal with {\term$_2$} and generates the
 equality {\term$_2$}{\tt =}{\term$_1$} as a subgoal. This equality is
-automatically solved if it occurs amongst the assumption, or if its
+automatically solved if it occurs among the assumption, or if its
 symmetric form occurs.  It is equivalent to {\tt cut
 \term$_2$=\term$_1$; [intro H{\sl n}; rewrite <- H{\sl n}; clear H{\sl
 n}| assumption || symmetry; try assumption]}.
@@ -3034,7 +3034,7 @@ computational expressions (i.e. with few dead code).
   \cite{CompiledStrongReduction}. This algorithm is dramatically more efficient
   than the algorithm used for the {\tt cbv} tactic, but it cannot be
   fine-tuned. It is specially interesting for full evaluation of algebraic
-  objects. This includes the case of reflexion-based tactics.
+  objects. This includes the case of reflection-based tactics.
 
 \item {\tt native\_compute} \tacindex{native\_compute}
 
@@ -4781,7 +4781,7 @@ Reset Initial.
 
 This tactic puts the {\num} first goals at the end of the list of
 goals. If {\num} is negative, it will put the last $\left|\num\right|$ goals at
-the begining of the list.
+the beginning of the list.
 
 \Example
 \begin{coq_example*}
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 48e2df19dc..76e4efd606 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -68,7 +68,7 @@ but also at the command {\tt Declare ML Module}.
 
 Dependencies of \ocaml\ modules are computed by looking at
 \verb!open! commands and the dot notation {\em module.value}. However,
-this is done approximatively and you are advised to use {\tt ocamldep}
+this is done approximately and you are advised to use {\tt ocamldep}
 instead for the \ocaml\ modules dependencies.
 
 See the man page of {\tt coqdep} for more details and options.
@@ -103,7 +103,7 @@ invocation
 While customizing a project file, mind the following requirements:
 \begin{itemize}
 \item {\Coq} files must end in \texttt{.v}, {\ocaml} modules in
-  \texttt{.ml4} if they require camlp preproccessing (and in
+  \texttt{.ml4} if they require camlp preprocessing (and in
   \texttt{.ml} otherwise), {\ocaml} module signatures, library
   description and packing files respectively in \texttt{.mli},
   \texttt{.mllib} and \texttt{.mlpack}.
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index dc88a00ead..91d30c0730 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -36,7 +36,7 @@
 \input{../common/title.tex}% extension .tex pour htmlgen
 %\input{headers}
 
-\usepackage[linktocpage,colorlinks]{hyperref}
+\usepackage[linktocpage,colorlinks,bookmarks=true,bookmarksnumbered=true]{hyperref}
 % The manual advises to load hyperref package last to be able to redefine
 % necessary commands.
 % The above should work for both latex and pdflatex. Even if PDF is produced