From 5e62675419fb6a5a8f8a86fbf3f6df4427e70d21 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 2 Oct 2015 16:50:26 +0200
Subject: Fixing error messages about Hint.

---
 doc/refman/RefMan-tac.tex | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 06431055ad..a21e5631fc 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3645,16 +3645,16 @@ The {\hintdef} is one of the following expressions:
   that is used only by \texttt{eauto} is a transitivity lemma.
 
   \begin{ErrMsgs}
-  \item \errindex{Bound head variable}
+%%  \item \errindex{Bound head variable}
+
+  \item \term\ \errindex{cannot be used as a hint}
 
     The head symbol of the type of {\term} is a bound variable such
     that this tactic cannot be associated to a constant.
 
-  \item \term\ \errindex{cannot be used as a hint}
-
-    The type of {\term} contains products over variables that do not
-    appear in the conclusion. A typical example is a transitivity axiom.
-    In that case the {\tt simple apply} tactic fails, and thus is useless.
+    %% The type of {\term} contains products over variables that do not
+    %% appear in the conclusion. A typical example is a transitivity axiom.
+    %% In that case the {\tt simple apply} tactic fails, and thus is useless.
 
   \end{ErrMsgs}
 
@@ -3684,7 +3684,7 @@ The {\hintdef} is one of the following expressions:
 
   \begin{ErrMsgs}
 
-  \item \errindex{Bound head variable}
+%%  \item \errindex{Bound head variable}
 
   \item \term\ \errindex{cannot be used as a hint}
 
@@ -3710,7 +3710,9 @@ The {\hintdef} is one of the following expressions:
 
     \item {\ident} \errindex{is not an inductive type}
 
-    \item {\ident} \errindex{not declared}
+% No need to have this message here, is is generic to all commands
+% referring to globals
+%%    \item {\ident} \errindex{not declared}
 
   \end{ErrMsgs}
 
-- 
cgit v1.2.3