From fe038eea4f1c62a209db18fadb69dbab80e16c16 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 29 Jan 2015 15:07:12 +0100
Subject: Remove some "Warning:" from the reference manual.

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

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

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 193479cceb..4b197ec738 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -167,7 +167,7 @@ defined with the {\tt Record} keyword can be activated with the
 (see~\ref{set-nonrecursive-elimination-schemes}).
 
 \begin{Warnings}
-\item {\tt Warning: {\ident$_i$} cannot be defined.}
+\item {\tt {\ident$_i$} cannot be defined.}
 
   It can happen that the definition of a projection is impossible.
   This message is followed by an explanation of this impossibility.
-- 
cgit v1.2.3


From db293d185f8deb091d4b086f327caa0f376d67d7 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 29 Jan 2015 20:04:22 +0100
Subject: Fix index of reference manual.

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

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

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 4b197ec738..3605a716e7 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -434,7 +434,7 @@ we have an equivalence between
 {\tt match {\term} \zeroone{\ifitem} with C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end}
 
 
-\subsubsection{Second destructuring {\tt let} syntax\index{let '... in}}
+\subsubsection{Second destructuring {\tt let} syntax\index{let '... in@\texttt{let '... in}}}
 
 Another destructuring {\tt let} syntax is available for inductive types with
 one constructor by giving an arbitrary pattern instead of just a tuple
@@ -2000,7 +2000,7 @@ variables, use
 \end{quote}
 
 \subsection{Solving existential variables using tactics}
-\index{\tt \textdollar( \ldots )\textdollar}
+\ttindex{\textdollar( \ldots )\textdollar}
 
 \def\expr{\textrm{\textsl{tacexpr}}}
 
-- 
cgit v1.2.3