Documenting the Loose Hint Behavior flag.

2 files changed, 51 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index 85a207c29f..cb77c297dd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,9 +7,18 @@ Vernacular commands
 
 Tactics
 
-- New flag "Set Regular Subst Tactic" which fixes "subst" in situations where
+- New flag "Regular Subst Tactic" which fixes "subst" in situations where
   it failed to substitute all substitutable equations or failed to simplify
   cycles, or accidentally unfolded local definitions (flag is off by default).
+- New flag "Loose Hint Behavior" to handle hints loaded but not imported in a
+  special way. It accepts three distinct flags:
+  * "Lax", which is the default one, sets the old behavior, i.e. a non-imported
+  hint behaves the same as an imported one.
+  * "Warn" outputs a warning when a non-imported hint is used. Note that this is
+  an over-approximation, because a hint may be triggered by an eauto run that
+  will eventually fail and backtrack.
+  * "Strict" changes the behavior of an unloaded hint to the one of the fail
+  tactic, allowing to emulate the hopefully future import-scoped hint mechanism.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 2eebac18e6..d1e9ec7960 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3853,6 +3853,7 @@ development.
 
 \subsection{\tt Remove Hints \term$_1$ \mbox{\dots} \term$_n$ :~ \ident$_1$
   \mbox{\dots} \ident$_m$}
+\label{RemoveHints}
 \comindex{Remove Hints}
 
 This command removes the hints associated to terms \term$_1$ \mbox{\dots}
@@ -3931,8 +3932,9 @@ main subgoal excluded.
 
 \end{Variants}
 
-\subsection{Hints and sections
-\label{Hint-and-Section}}
+\subsection{Hint locality
+\label{Hint-Locality}}
+\optindex{Loose Hint Behavior}
 
 Hints provided by the \texttt{Hint} commands are erased when closing a
 section. Conversely, all hints of a module \texttt{A} that are not
@@ -3940,6 +3942,43 @@ defined inside a section (and not defined with option {\tt Local}) become
 available when the module {\tt A} is imported (using
 e.g. \texttt{Require Import A.}).
 
+As of today, hints only have a binary behavior regarding locality, as described
+above: either they disappear at the end of a section scope, or they remain
+global forever. This causes a scalability issue, because hints coming from an
+unrelated part of the code may badly influence another development. It can be
+mitigated to some extent thanks to the {\tt Remove Hints} command
+(see ~\ref{RemoveHints}), but this is a mere workaround and has some
+limitations (for instance, external hints cannot be removed).
+
+A proper way to fix this issue is to bind the hints to their module scope, as
+for most of the other objects Coq uses. Hints should only made available when
+the module they are defined in is imported, not just required. It is very
+difficult to change the historical behavior, as it would break a lot of scripts.
+We propose a smooth transitional path by providing the {\tt Loose Hint Behavior}
+option which accepts three flags allowing for a fine-grained handling of
+non-imported hints.
+
+\begin{Variants}
+
+\item {\tt Set Loose Hint Behavior "Lax"}
+
+  This is the default, and corresponds to the historical behavior, that is,
+  hints defined outside of a section have a global scope.
+
+\item {\tt Set Loose Hint Behavior "Warn"}
+
+  When set, it outputs a warning when a non-imported hint is used. Note that
+  this is an over-approximation, because a hint may be triggered by a run that
+  will eventually fail and backtrack, resulting in the hint not being actually
+  useful for the proof.
+
+\item {\tt Set Loose Hint Behavior "Strict"}
+
+  When set, it changes the behavior of an unloaded hint to a immediate fail
+  tactic, allowing to emulate an import-scoped hint mechanism.
+
+\end{Variants}
+
 \subsection{Setting implicit automation tactics}
 
 \subsubsection{\tt Proof with {\tac}}