Imported Upstream version 8.3pl1upstream/8.3pl1

6 files changed, 85 insertions, 27 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index de1d84be..bd6f7dbf 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -97,6 +97,7 @@
 \def\symmetryin{{\tt symmetryin}}
 \def\instantiate{{\tt instantiate}}
 \def\inversion{{\tt inversion}}
+\def\specialize{{\tt specialize}}
 \def\Defined{{\tt Defined}}
 \def\Qed{{\tt Qed}}
 \def\pattern{{\tt pattern}}
@@ -868,6 +869,16 @@ provide names for these variables: {\Coq} will do it anyway, but such
 automatic naming decreases legibility and robustness.
 
 
+\Question{My goal contains an universally quantified statement, how can I use it?}
+
+If the universally quantified assumption matches the goal you can
+use the {\apply} tactic. If it is an equation you can use the
+{\rewrite} tactic. Otherwise you can use the {\specialize} tactic
+to instantiate the quantified variables with terms. The variant
+{\tt assert(Ht := H t)} makes a copy of assumption {\tt H} before
+instantiating it.
+
+
 \Question{My goal is an existential, how can I prove it?}
 
 Use some theorem or assumption or exhibit the witness using the {\existstac} tactic.
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 7bd4f352..f427609f 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -10,7 +10,7 @@
 \label{typeclasses}
 
 \begin{flushleft}
-  \em The status of Type Classes is (extremely) experimental.
+  \em The status of Type Classes is experimental.
 \end{flushleft}
 
 This chapter presents a quick reference of the commands related to type
@@ -128,9 +128,7 @@ particular support for type classes:
   methods. In the example above, \texttt{A} and \texttt{eqa} should be
   set maximally implicit.
 \item They support implicit quantification on partialy applied type
-  classes (\S \ref{implicit-generalization}).
-  Any argument not given as part of a type class binder will be
-  automatically generalized.
+  classes.
 \item They also support implicit quantification on superclasses
   (\S \ref{classes:superclasses})
 \end{itemize}
@@ -143,6 +141,19 @@ Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).
 Here \texttt{A} is implicitly generalized, and the resulting function
 is equivalent to the one above.
 
+The parsing of generalized type-class binders is different from regular
+binders:
+\begin{itemize}
+\item Implicit arguments of the class type are ignored.
+\item Superclasses arguments are automatically generalized.
+\item Any remaining arguments not given as part of a type class binder
+  will be automatically generalized. In other words, the rightmost
+  parameters are automatically generalized if not mentionned.
+\end{itemize}
+
+One can switch off this special treatment using the $!$ mark in front of
+the class name (see example below).
+
 \asection{Parameterized Instances}
 
 One can declare parameterized instances as in \Haskell simply by giving
@@ -231,9 +242,9 @@ Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x).
 \end{coq_example*}
 
 In some cases, to be able to specify sharing of structures, one may want to give
-explicitly the superclasses. It is is possible to do it directly in regular
-binders, and using the \texttt{!} modifier in class binders. For
-example:
+explicitly the superclasses. It is possible to do it directly in regular
+generalized binders, and using the \texttt{!} modifier in class
+binders. For example:
 \begin{coq_example*}
 Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := 
   andb (le x y) (neqb x y).
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 9efa7048..b8a893d5 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1622,7 +1622,7 @@ the generalized variables. Inside implicit generalization
 delimiters, free variables in the current context are automatically
 quantified using a product or a lambda abstraction to generate a closed
 term. In the following statement for example, the variables \texttt{n}
-and \texttt{m} are autamatically generalized and become explicit
+and \texttt{m} are automatically generalized and become explicit
 arguments of the lemma as we are using \verb|`( )|:
 
 \begin{coq_example}
@@ -1638,7 +1638,7 @@ generalizations when mistyping identifiers. There are three variants of
 the command:
 
 \begin{quote}
-{\tt Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.}
+{\tt (Global)? Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.}
 \end{quote}
 
 \begin{Variants}
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index 04830531..5d9c8c16 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -261,26 +261,32 @@ CONTROL and the SHIFT keys, and type the hexadecimal code of the
 symbol required, for example \verb|2200| for the $\forall$ symbol.
 A list of symbol codes is available at \url{http://www.unicode.org}. 
 
-This method obviously doesn't scale, that's why the preferred alternative is to
-use an Input Method Editor. On POSIX systems (Linux distros, BSD variants and
-MacOS X), you can use \texttt{uim} version 1.6 or later which provides a \LaTeX{}-style
-input method.
-
-To configure \texttt{uim}, execute \texttt{uim-pref-gtk} as your regular user.
-In the "Global Settings" group set the default Input Method to "ELatin" (don't
-forget to tick the checkbox "Specify default IM"). In the "ELatin" group set the
-layout to "TeX", and remember the content of the "[ELatin] on" field (by default
-"<Control>\"). You can now execute CoqIDE with the following commands (assuming
-you use a Bourne-style shell):
+This method obviously doesn't scale, that's why the preferred
+alternative is to use an Input Method Editor. On POSIX systems (Linux
+distributions, BSD variants and MacOS X), you can use \texttt{uim} to
+support \LaTeX{}-style edition and, if using X Windows, you can also use
+the XCompose method (XIM). How to use \texttt{uim} is documented below.
+
+If you have \texttt{uim} 1.5.x, first manually copy the files located
+in directory {\tt ide/uim} of the Coq source distribution to the
+{\tt uim} directory of input methods which typically is {\tt
+  /usr/share/uim}. Execute {\tt uim-module-manager -{-}register
+  coqide}. Then, execute \texttt{uim-pref-gtk} as regular user and set
+the default Input Method to "CoqIDE" in the "Global Settings" group
+(don't forget to tick the checkbox "Specify default IM"; you may also
+have to first edit the set of "Enabled input method" to add CoqIDE to
+the set). You can now execute CoqIDE with the following commands
+(assuming you use a Bourne-style shell):
 
 \begin{verbatim}
 $ export GTK_IM_MODULE=uim
 $ coqide
 \end{verbatim}
 
-Activate the ELatin Input Method with Ctrl-\textbackslash, then type the
-sequence "\verb=\Gamma=". You will see the sequence being
-replaced by $\Gamma$ as soon as you type the second "a".
+If you then type the sequence "\verb=\Gamma=", you will see the sequence being
+replaced by $\Gamma$ as soon as you  type the second "a".
+
+If you have \texttt{uim} 1.6.x, the \LaTeX{} input method is built-in. You just have to execute \texttt{uim-pref-gtk} and choose "ELatin" as default Input Method in the "Global Settings". Then, in the "ELatin" group set the layout to "TeX", and remember the content of the "[ELatin] on" field (by default "<Control>$\backslash$"). Proceed then as above.
 
 \subsection[Character encoding for saved files]{Character encoding for saved files\label{sec:coqidecharencoding}}
 
@@ -314,7 +320,7 @@ or
 
     
 
-% $Id: RefMan-ide.tex 13477 2010-09-30 16:50:00Z vgross $ 
+% $Id: RefMan-ide.tex 13701 2010-12-10 07:48:30Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b82cdc2d..450d3b2d 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -989,6 +989,36 @@ Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals
 have names of the form {\ident}\texttt{\_admitted} possibly followed
 by a number.
 
+\subsection{\tt constr\_eq \term$_1$ \term$_2$
+\tacindex{constr\_eq}
+\label{constreq}}
+
+This tactic applies to any goal. It checks whether its arguments are
+equal modulo alpha conversion and casts.
+
+\ErrMsg \errindex{Not equal}
+
+\subsection{\tt is\_evar \term
+\tacindex{is\_evar}
+\label{isevar}}
+
+This tactic applies to any goal. It checks whether its argument is an
+existential variable. Existential variables are uninstantiated
+variables generated by e.g. {\tt eapply} (see Section~\ref{apply}).
+
+\ErrMsg \errindex{Not an evar}
+
+\subsection{\tt has\_evar \term
+\tacindex{has\_evar}
+\label{hasevar}}
+
+This tactic applies to any goal. It checks whether its argument has an
+existential variable as a subterm. Unlike {\tt context} patterns
+combined with {\tt is\_evar}, this tactic scans all subterms,
+including those under binders.
+
+\ErrMsg \errindex{No evars}
+
 \subsection{Bindings list
 \index{Binding list}
 \label{Binding-list}}
@@ -3917,7 +3947,7 @@ where {\sl hint\_definition} is one of the following expressions:
 
 \begin{quotation}
 \begin{verbatim}
-Hint Extern 4 ~(?=?) => discriminate.
+Hint Extern 4 (~(_ = _)) => discriminate.
 \end{verbatim}
 \end{quotation}
 
@@ -4294,7 +4324,7 @@ Chapter~\ref{TacticLanguage} gives examples of more complex
 user-defined tactics.
 
 
-% $Id: RefMan-tac.tex 13344 2010-07-28 15:04:36Z msozeau $ 
+% $Id: RefMan-tac.tex 13659 2010-11-29 11:09:07Z glondu $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 63c35548..723295bf 100755
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -1574,4 +1574,4 @@ with \Coq, in order to acquaint yourself with various proof techniques.
 
 \end{document}
 
-% $Id: Tutorial.tex 13548 2010-10-14 12:35:43Z notin $ 
+% $Id: Tutorial.tex 13547 2010-10-14 12:35:00Z notin $