From 5be957316c23db6366aefc246d1d24480aa2f1ea Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 19 Oct 2016 14:18:52 +0200
Subject: Making the doc of auto hints more precise.

The doc of auto hints now mention again that sometimes a hint
will be used with simple apply and sometimes it will be used
with exact.
It does not try to be fully precise in that we don't
necessarily want to document the behaviors of auto that
we might like to change.
See also the discussion on commit 9227d6e.
---
 doc/refman/RefMan-tac.tex | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 49a5b7983a..263766b272 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3709,11 +3709,12 @@ The {\hintdef} is one of the following expressions:
   the number of subgoals generated by {\tt simple apply {\term}}.
 %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false
 
-  % Is it really needed?
-  %% In case the inferred type of \term\ does not start with a product
-  %% the tactic added in the hint list is {\tt exact {\term}}. In case
-  %% this type can however be reduced to a type starting with a product,
-  %% the tactic {\tt apply {\term}} is also stored in the hints list.
+  In case the inferred type of \term\ does not start with a product
+  the tactic added in the hint list is {\tt exact {\term}}.
+% Actually, a slightly restricted version is used (no conversion on the head symbol)
+  In case
+  this type can however be reduced to a type starting with a product,
+  the tactic {\tt simple apply {\term}} is also stored in the hints list.
 
   If the inferred type of \term\ contains a dependent quantification
   on a variable which occurs only in the premisses of the type and not
-- 
cgit v1.2.3