summaryrefslogtreecommitdiff
path: root/doc/refman
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman')
-rw-r--r--doc/refman/Classes.tex25
-rw-r--r--doc/refman/RefMan-ext.tex4
-rw-r--r--doc/refman/RefMan-ide.tex36
-rw-r--r--doc/refman/RefMan-tac.tex34
4 files changed, 73 insertions, 26 deletions
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