Add user syntax for creating hint databases [Create HintDb foo

[discriminated]] with a switch for using the more experimantal dnet impl
for every hint. Also add [Hint Transparent/Opaque] which parameterize
the dnet and the unification flags used by auto/eauto with a particular
database. Document all this. Remove [Typeclasses unfold] directives that
are no longer needed (everything is unfoldable by default) and move to
[Typeclasses Transparent/Opaque] syntax.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11409 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 65 insertions, 7 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 54237d721..bb845beb1 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3598,10 +3598,44 @@ The hints for \texttt{auto} and \texttt{eauto} are stored in
 databases.  Each database maps head symbols to a list of hints. One can
 use the command \texttt{Print Hint \ident} to display the hints
 associated to the head symbol \ident{} (see \ref{PrintHint}). Each
-hint has a cost that is an nonnegative integer, and a pattern. 
+hint has a cost that is an nonnegative integer, and an optional pattern. 
 The hints with lower cost are tried first. A hint is tried by 
 \texttt{auto} when the conclusion of the current goal
-matches its pattern. The general
+matches its pattern or when it has no pattern. 
+
+\subsubsection*{Creating Hint databases
+  \label{CreateHintDb}\comindex{CreateHintDb}}
+
+One can optionally declare a hint database using the command
+\texttt{Create HintDb}. If a hint is added to an unknown database, it
+will be automatically created. 
+
+\medskip
+\texttt{Create HintDb} {\ident} [\texttt{discriminated}]
+\medskip
+
+This command creates a new database named \ident. There are two
+implementations of hint databases available. One uses a
+discrimination network which is parameterized by transparency information
+for all hints and all goals, including those that contain
+existential variables, the other one uses the discrimination net only on
+goals without existentials, for non-Immediate hints and do not make
+use of transparency hints (the default).
+The performance of discriminated hint databases can be improved by
+adding transparency hints that make the network more constrained
+(c.f. \ref{HintTransparency}).
+
+\begin{Variants}
+\item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:}
+  \ident$_1$ \ldots\ \ident$_n$
+  
+  This is used to declare a hint database that must not be exported to the other
+  modules that require and import the current module. Inside a
+  section, the option {\tt Local} is useless since hints do not
+  survive anyway to the closure of sections.
+\end{Variants}
+
+The general
 command to add a hint to some database \ident$_1$, \dots, \ident$_n$ is:
 \begin{tabbing}
   \texttt{Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ \ldots\ \ident$_n$
@@ -3721,12 +3755,31 @@ where {\sl hint\_definition} is one of the following expressions:
 
   \end{Variants}
 
-\item \texttt{Extern \num\ \pattern\ => }\textsl{tactic}
+\item \texttt{Transparent},\texttt{Opaque} {\qualid}
+\label{HintTransparency}
+\comindex{Hint Transparent}
+\comindex{Hint Opaque}
+  
+  This adds a transparency hint to the database, making {\tt {\qualid}}
+  a transparent or opaque constant during resolution. This information 
+  is used during unification of the goal with any lemma in the database
+  and inside the discrimination network to relax or constrain it in the
+  case of \texttt{discriminated} databases.
+  
+  \begin{Variants}
+
+    \item \texttt{Transparent},\texttt{Opaque} {\ident$_1$} \dots {\ident$_m$} 
+
+      Declares each {\ident$_i$} as a transparent or opaque constant.
+      
+  \end{Variants}
+
+\item \texttt{Extern \num\ [\pattern]\ => }\textsl{tactic}
 \comindex{Hint Extern}
 
   This hint type is to extend \texttt{auto} with tactics other than
   \texttt{apply} and \texttt{unfold}. For that, we must specify a
-  cost, a pattern and a tactic to execute. Here is an example:
+  cost, an optional pattern and a tactic to execute. Here is an example:
 
 \begin{quotation}
 \begin{verbatim}
@@ -3737,7 +3790,7 @@ Hint Extern 4 ~(?=?) => discriminate.
   Now, when the head of the goal is a disequality, \texttt{auto} will
   try \texttt{discriminate} if it does not succeed to solve the goal
   with hints with a cost less than 4.
-
+  
   One can even use some sub-patterns of the pattern in the tactic
   script. A sub-pattern is a question mark followed by an ident, like
   \texttt{?X1} or \texttt{?X2}. Here is an example:
@@ -3759,8 +3812,9 @@ Abort.
 
 \end{itemize}
 
-\Rem There is currently (in the \coqversion\ release) no way to do
-pattern-matching on hypotheses.
+\Rem One can use an \texttt{Extern} hint with no pattern to do
+pattern-matching on hypotheses using \texttt{match goal with} inside 
+the tactic.
 
 \begin{Variants}
 \item \texttt{Hint} \textsl{hint\_definition} 
@@ -3838,6 +3892,10 @@ databases are non empty and can be used.
 
 \item[\tt sets] contains lemmas about sets and relations from the 
   directories \texttt{Sets} and \texttt{Relations}.
+
+\item[\tt typeclass\_instances] contains all the type class instances
+  declared in the environment, including those used for \texttt{setoid\_rewrite},
+  from the \texttt{Classes} directory.
 \end{description}
 
 There is also a special database called {\tt v62}. It collects all