From 253493355a71c0673b0c10b06e7eb9f0fd0242a9 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 17 Nov 2016 16:01:29 +0100
Subject: Add missing label. Fixes broken ref.

---
 doc/refman/Classes.tex | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc')

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index bd8ee450ef..acfc4bea93 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -380,6 +380,7 @@ use implicit generalization (see \ref{SectionContext}).
 
 \asubsection{\tt typeclasses eauto}
 \tacindex{typeclasses eauto}
+\label{typeclasseseauto}
 
 The {\tt typeclasses eauto} tactic uses a different resolution engine
 than {\tt eauto} and {\tt auto}. The main differences are the following:
-- 
cgit v1.2.3


From 08c6e4c3dbe2ae851ef3097cc44618ea82717974 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Mon, 5 Dec 2016 17:26:55 -0500
Subject: the -byte option is deprecated

---
 doc/refman/RefMan-com.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index c1e552a5da..784c9ccbbf 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -26,8 +26,8 @@ run by the command {\tt coqtop}.
 They are two different binary images of \Coq: the byte-code one and
 the native-code one (if {\ocaml} provides a native-code compiler
 for your platform, which is supposed in the following). By default,
-\verb!coqc! executes the native-code version; this can be overridden
-using the \verb!-byte! option.
+\verb!coqtop! executes the native-code version; run \verb!coqtop.byte! to
+get the byte-code version.
 
 The byte-code toplevel is based on an {\ocaml}
 toplevel (to allow the dynamic link of tactics).  You can switch to
-- 
cgit v1.2.3


From 2125949733b631426e955e722d6ca4e1b2eb5b60 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Mon, 5 Dec 2016 17:55:15 -0500
Subject: Change module for Coq loop

---
 doc/refman/RefMan-com.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 784c9ccbbf..bef0a1686f 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -32,7 +32,7 @@ get the byte-code version.
 The byte-code toplevel is based on an {\ocaml}
 toplevel (to allow the dynamic link of tactics).  You can switch to
 the {\ocaml} toplevel with the command \verb!Drop.!, and come back to the
-\Coq~toplevel with the command \verb!Toplevel.loop();;!.
+\Coq~toplevel with the command \verb!Coqloop.loop();;!.
 
 \section{Batch compilation ({\tt coqc})}
 The {\tt coqc} command takes a name {\em file} as argument.  Then it
-- 
cgit v1.2.3


From 227ff6a46ad511ff2ab0ba1ffb9017bdb0291a58 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 6 Dec 2016 17:52:26 +0100
Subject: Update documentation (bugs #5246 and #5251).

---
 doc/refman/RefMan-gal.tex | 6 +++---
 doc/refman/RefMan-tac.tex | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 99eee44e03..3814e4403a 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -713,9 +713,9 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt
            {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\
  & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\
            & & \\
-{\inductivebody} & ::= & 
-  {\ident} \zeroone{\binders} {\tt :} {\term} {\tt :=} \\
-   && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstrwithoutblank}}{|}} \\
+{\inductivebody} & ::= &
+  {\ident} \zeroone{\binders} {\typecstr} {\tt :=} \\
+   && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstr}}{|}} \\
            & & \\  %% TODO: where ...
 %% Fixpoints
 {\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} {\tt .} \\
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 01dc1dec9b..4b06520314 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -302,7 +302,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form
 {\tt (fun $x$ => $Q$)~$u_1$~\ldots~$u_n$}.
 
 \begin{ErrMsgs}
-\item \errindex{Impossible to unify \dots\ with \dots}
+\item \errindex{Unable to unify \dots\ with \dots}
 
   The {\tt apply}
   tactic failed to match the conclusion of {\term} and the current goal.
@@ -4621,7 +4621,7 @@ It is equivalent to {\tt apply refl\_equal}.
 
 \begin{ErrMsgs}
 \item \errindex{The conclusion is not a substitutive equation}
-\item \errindex{Impossible to unify \dots\ with \dots}
+\item \errindex{Unable to unify \dots\ with \dots}
 \end{ErrMsgs}
 
 \subsection{\tt symmetry}
-- 
cgit v1.2.3


From 7af1b3e08452c3bbced6ca7eece2c91c6bf29137 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 6 Dec 2016 18:53:22 +0100
Subject: Fix broken documentation in presence of \zeroone{... \tt ...}.

The way \zeroone was defined, the \tt modifier was leaked outside the
brackets, thus messing with the following text. There are a bunch of
occurrences of this issue in the manual, so rather than turning all the
\tt into \texttt, the definition of \zeroone is made more robust.

Unfortunately, there is one single occurrence of \zeroone that does not
support the more robust version. (Note that this specific usage of
\zeroone is morally a bug, since it goes against all the LaTeX
conventions.) So the commit also keeps the old leaky version of \zeroone
around as \zeroonelax so that it can be used there.
---
 doc/common/macros.tex     | 3 ++-
 doc/refman/RefMan-tac.tex | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index df5ee405f9..5abdecfc18 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -72,7 +72,8 @@
 %\newcommand{\spec}[1]{\{\,#1\,\}}
 
 % Building regular expressions
-\newcommand{\zeroone}[1]{\mbox{\sl [}#1\mbox{\sl ]}}
+\newcommand{\zeroone}[1]{\mbox{\sl [}{#1}\mbox{\sl ]}}
+\newcommand{\zeroonelax}[1]{\mbox{\sl [}#1\mbox{\sl ]}}
 %\newcommand{\zeroonemany}[1]{$\{$#1$\}$*}
 %\newcommand{\onemany}[1]{$\{$#1$\}$+}
 \newcommand{\nelistnosep}[1]{{#1} \mbox{\dots} {#1}}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 4b06520314..3f12411863 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -114,7 +114,7 @@ following syntax:
 \begin{tabular}{lcl}
 {\occclause} & ::= & {\tt in} {\occgoalset} \\
 {\occgoalset} & ::= &
-    \zeroone{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\
+    \zeroonelax{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\
 &   & {\dots} {\tt ,}\\
 &   & {\ident$_m$} \zeroone{\atoccurrences}}\\
 &   & \zeroone{{\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}}\\
-- 
cgit v1.2.3