MAJ Search

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

2 files changed, 178 insertions, 53 deletions

diff --git a/doc/Changes.tex b/doc/Changes.tex
index 4eac456338..15ecb8ea98 100755
--- a/doc/Changes.tex
+++ b/doc/Changes.tex
@@ -8,85 +8,216 @@
 \begin{document}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Changes 6.3 ===> 6.3.1
+% Changes 6.3.1 ===> 7.0
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\shorttitle{Changes from {\Coq} V6.3 to {\Coq} V6.3.1}
+\shorttitle{Changes from {\Coq} V6.3.1 to {\Coq} V7}
 
-This document describes the main differences between Coq V6.3 and
+This document describes the main differences between Coq V7 and
 V6.3.1. This new version of Coq is characterized by fixed bugs, and
 improvement of implicit arguments synthesis and speed in tactic
 applications.
 
 \section{Changes overview}
 
-\subsection{Tactics}
+The new major version number is explained by a deep restructuration of
+the implementation code of Coq. From a user point of view, Coq V7 is
+characterized by the following novelties:
+
+\begin{itemize}
+\item A mini-language to write tactics with high-level
+pattern-matching on goals  (see section \ref{Tactics})
+
+\item A primitive let-in constructions (see section \ref{Metatheory})
+\item Structuration of the name space and access to names by the dot notation (see section \ref{Metatheory})
+\item A command to export theories to XML to be used with rendering
+tools by Bologna University (see section \ref{Tools})
+\item Various improvements, including a search facilities by pattern
+provided by Yves Bertot (see section \ref{Tools})
+\item As usual, several bugs fixed and a lot of new ones introduced
+\end{itemize}
+
+Incompatibilities are described in section
+\ref{Incompatibilities}. Please notice that extraction and the
+{\texttt Program/Realizer} tactic are unavailable in Coq V7.
+Developpers of tactics in ML are invited to read section
+\ref{Developers}.
+
+\section{Tactics}
+\label{Tactics}
+\def\ltac{{\cal L}_{tac}}
 
-  \begin{itemize}
+\begin{description}
 
-  \item \texttt {Tauto} has been unable for a time to deal with
-hypotheses with 2 imbricated implications. Now it should work.
-\texttt {Intuition} now removes true, and therefore useless,
-hypotheses.\\
+\item[The main novelty is $\ltac$,] a mini-language contributed
+by David Delahaye to write tactics with high-level pattern-matching on
+goals. A separate documentation entitled $\ltac$ is available
+in the archive or at the author page
+http://logical.inria.fr/~delahaye.
 
-  \item Several bugs of the {\texttt Program} are fixed (but some
-  automatically generated names have changed and may lead to
-  incompatibilities).
 
-  \item Bug with negative index in bindings fixed.
+\item[Other changes]
+
+  \begin{itemize}
 
-  \item Speed improvement: redondant checks when applying a tactic
-  have been turned off. For some tactics that don't make themselves
-  the expected verifications, it may result in incorrect proofs
-  detected only at Qed/Save time. In this last case, you can turn on
-  the -tac-debug flag to coqtop.
+  \item {\texttt Tauto} and {\texttt Intuition} has been rewritten in
+$\ltac$. This has introduced some changes in the hypotheses names
+generated by {\texttt Intuition}. The previous versions of {\texttt
+Tauto} and {\texttt Intuition} remains available under the names ???.\\
 
-  \item The ``?'' in goals are now instantiated as soon as an instance
-  is known for them.
+  \item	Redondant or incompatible instantiations in {\texttt
+  Apply ... with ...} now correctly trapped
 
   \end{itemize}
 
-\subsection{Toplevel commands}
+  \item[Program/Realizer] is unavailable in Coq V7.
+
+\end{description}
+
+\section{Toplevel commands}
 
 \begin{description}
     
-\item Bug in \texttt{Time} fixed.
+\item[New searching mechanism by pattern] contributed by Yves Bertot
+
+\begin{itemize}
+
+\item {\texttt SearchPattern {\term}.}
+
+This command displays the name and type of all theorems of the current
+context whose statement's conclusion matches the expression {\term}
+where holes in the latter are denoted by ``{\texttt ?}''.
+
+\begin{coq_example}
+Require Arith.
+SearchPattern (plus ? ?)=?.
+\end{coq_example}
+
+Patterns need not be linear: you can express that the same
+expression must occur in two places by using indexed `{\texttt ?}''.
+
+\begin{coq_example}
+Require Arith.
+SearchPattern (plus ?1 ?)=?1.
+\end{coq_example}
+
+\item {\texttt SearchRewrite {\term}.}
+
+This command displays the name and type of all theorems of the current
+context whose statement's conclusion is an equality of which one side matches
+the expression {\term =}. Holes in {\term} are denoted by ``{\texttt ?}''.
+
+\begin{coq_example}
+Require Arith.
+SearchRewrite (plus ? ?).
+\end{coq_example}
+\end{itemize}
+
+\begin{Variants}
+\item {\tt SearchPattern {\term} inside {\module$_1$}...{\module$_n$}}\\
+  This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}.
+
+\item {\tt SearchPattern {\term} outside {\module}.}\\
+  This restricts the search to constructions not defined in modules
+{\module$_1$}...{\module$_n$}.
+
+\item {\tt SearchRewrite {\term} inside
+{\module$_1$}...{\module$_n$}.}\\
+  This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}.
+
+\item {\tt SearchRewrite {\term} outside {\module$_1$}...{\module$_n$}.}\\
+  This restricts the search to constructions not defined in modules {\module$_1$}...{\module$_n$}.
+
+\end{Variants}
+
+\item {\texttt Search {\ident}} has been extended to accept qualified
+identifiers and the {\tt inside} and {\tt outside} restrictions as
+{\texttt SearchPattern} and {\texttt SearchRewrite}.
 
 \end{description}
-    
-\subsection{Language}
 
-  \begin{description} \item[Type reconstruction] The algorithm to
-  solve incomplete information in terms has been improved
-  furthermore. In particular question marks can be put in in place of
-  the type of abstracted variables and in Cases expressions.
+\section{Language}
+\label{Language}
+
+\subsection{Names}
+
+\begin{description}
+
+\item[Structured absolute names] The naming strategy for constructions
+has been made clearer. A Coq name is now unique and has the form
+
+\begin{quote}
+{\texttt Coq.Init.Logic.Equality.eq}
+\end{quote}
+
+{\texttt eq} is the name of the construction.
+
+{\texttt Coq} means {\texttt eq} is a construction of the standard library of
+Coq.
+
+{\texttt Init} means it is defined in directory {\texttt Init} of the
+standard library of Coq.
+
+{\texttt Logic} means it is defined in file {\texttt Logic.v} of the
+directory {\texttt Init} in the standard library of Coq.
 
-  \item[Guarded cofixpoints] A weakness in the guardness condition
-  when a cofixpoint refers to another one has been corrected.
-  WARNING: the new criterion may refuse some olderly accepted
-  Cofixpoint definitions which actually are valid but for a reason
-  difficult to detect automatically.
+{\texttt Equality} means it is defined in section {\texttt Equality}
+of the file {\texttt Logic.v} in the directory {\texttt Init} of the
+standard library of Coq.
 
-  \item[Extraction] A bug was limiting the number of propositional
-  singleton inductive types (such has ``eq'') for which elimination
-  towards Set is valid.
+Of course, there is no limit to the number of directory to traverse to
+find the corresponding file and no limit to the number of section to
+traverse in the file to find the corresponding definition.
 
-  \end{description}
+\item[Dot notation] Almost all commands accept the ``.'' notation to
+write absolute names.
 
-\subsection{Incompatibilities}
+\item[Open mechanism] Usually all required modules ({\texttt .vo}
+files) and closed sections are ``open'' by default. This means that
+constructions there can be accessed just by their identifier.
+
+
+\item[Bug] with identifiers ended by a number greater than $2^{31}$ fixed.
+
+\end{description}
+
+\section{Tools}
+\label{Tools}
+
+\begin{description}
+
+\item[Consistency check for {\texttt .vo} files] A check-sum test
+avoids to require inconsistent {\texttt .vo} files.
+
+\item[Optimal compiler] If your architecture supports it, the native
+version of {\texttt coqtop} and {\texttt coqc} is used by default.
+
+\item[Miscellaneous]
+
+\begin{itemize}
+\item {\texttt do\_Makefile} is now called {\texttt coq\_makefile}.
+
+\end{itemize}
+\end{description}
+
+\section{Incompatibilities}
+\label{Incompatibilities}
 
   You could have to modify your vernacular source for the following
   reasons:
 
   \begin{itemize}
  
-  \item Some names of variables generated by the \texttt{Program} have
-   changed.
-
-  \item {\texttt Intuition} now remove trye hypotheses.
+  \item {\texttt Intuition} now remove true hypotheses.
 
   \item In all cases, the ``.vo'' files are not compatible and should
   be recompiled.
 
+  \item[Extraction] is currently unavailable in Coq V7.
+
+  \item[Program/Realizer] tactics are currently unavailable in Coq V7.
+
+  \item[Linear] tactic is discontinued.
+
   \end{itemize}
 
 \section{New users contributions}
diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index 1018ca460e..91b89650b0 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -170,26 +170,20 @@ SearchRewrite (plus ? ?).
 
 \begin{Variants}
 \item
- {\tt Search {\qualid} inside
+{\tt Search {\qualid} inside
 {\module$_1$}...{\module$_n$}.}\comindex{Search ... inside ...}\\
 {\tt SearchPattern {\term} inside
 {\module$_1$}...{\module$_n$}.}\comindex{SearchPattern ... inside
 ...}\\
 {\tt SearchRewrite {\term} inside
-{\module$_1$}...{\module$_n$}.}\comindex{SearchRewrite ... inside ...}\\
+{\module$_1$}...{\module$_n$}.}\comindex{SearchRewrite ... inside ...}
+
 This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}.
 
 \item {\tt Search {\qualid} outside {\module$_1$}...{\module$_n$}.}\comindex{Search ... outside ...}\\
-  This restricts the search to constructions not defined in modules {\module$_1$}...{\module$_n$}.
-
-
-  This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}.
-
-\item {\tt SearchPattern {\term} outside {\module$_1$}...{\module$_n$}.}\comindex{SearchPattern ... outside ...}\\
-  This restricts the search to constructions not defined in modules
-{\module$_1$}...{\module$_n$}.
+{\tt SearchPattern {\term} outside {\module$_1$}...{\module$_n$}.}\comindex{SearchPattern ... outside ...}\\
+{\tt SearchRewrite {\term} outside {\module$_1$}...{\module$_n$}.}\comindex{SearchRewrite ... outside ...}
 
-\item {\tt SearchRewrite {\term} outside {\module$_1$}...{\module$_n$}.}\comindex{SearchRewrite ... outside ...}\\
   This restricts the search to constructions not defined in modules
 {\module$_1$}...{\module$_n$}.