1 files changed, 0 insertions, 412 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
deleted file mode 100644
index 7bd4f352..00000000
--- a/doc/refman/Classes.tex
+++ /dev/null
@@ -1,412 +0,0 @@
-\def\Haskell{\textsc{Haskell}\xspace}
-\def\eol{\setlength\parskip{0pt}\par}
-\def\indent#1{\noindent\kern#1}
-\def\cst#1{\textsf{#1}}
-
-\newcommand\tele[1]{\overrightarrow{#1}}
-
-\achapter{\protect{Type Classes}}
-\aauthor{Matthieu Sozeau}
-\label{typeclasses}
-
-\begin{flushleft}
-  \em The status of Type Classes is (extremely) experimental.
-\end{flushleft}
-
-This chapter presents a quick reference of the commands related to type
-classes. For an actual introduction to type classes, there is a
-description of the system \cite{sozeau08} and the literature on type
-classes in \Haskell which also applies.
-
-\asection{Class and Instance declarations}
-\label{ClassesInstances}
-
-The syntax for class and instance declarations is the same as
-record syntax of \Coq:
-\def\kw{\texttt}
-\def\classid{\texttt}
-
-\begin{center}
-\[\begin{array}{l}
-\kw{Class}~\classid{Id}~(\alpha_1 : \tau_1) \cdots (\alpha_n : \tau_n) 
-[: \sort] := \{\\
-\begin{array}{p{0em}lcl}
-  & \cst{f}_1 & : & \type_1 ; \\
-  & \vdots & &  \\
-  & \cst{f}_m & : & \type_m \}.
-\end{array}\end{array}\]
-\end{center}
-\begin{center}
-\[\begin{array}{l}
-\kw{Instance}~\ident~:~\classid{Id}~\term_1 \cdots \term_n := \{\\
-\begin{array}{p{0em}lcl}
-  & \cst{f}_1 & := & \term_{f_1} ; \\
-  & \vdots & &  \\
-  & \cst{f}_m & := & \term_{f_m} \}.
-\end{array}\end{array}\]
-\end{center}
-\begin{coq_eval}
-  Reset Initial.
-  Generalizable All Variables.
-\end{coq_eval}
-
-The $\tele{\alpha_i : \tau_i}$ variables are called the \emph{parameters}
-of the class and the $\tele{f_k : \type_k}$ are called the
-\emph{methods}. Each class definition gives rise to a corresponding
-record declaration and each instance is a regular definition whose name
-is given by $\ident$ and type is an instantiation of the record type.
-
-We'll use the following example class in the rest of the chapter:
-
-\begin{coq_example*}
-Class EqDec (A : Type) := {
-  eqb : A -> A -> bool ;
-  eqb_leibniz : forall x y, eqb x y = true -> x = y }.
-\end{coq_example*}
-
-This class implements a boolean equality test which is compatible with
-Leibniz equality on some type. An example implementation is:
-
-\begin{coq_example*}
-Instance unit_EqDec : EqDec unit :=
-{ eqb x y := true ;
-  eqb_leibniz x y H := 
-    match x, y return x = y with tt, tt => refl_equal tt end }.
-\end{coq_example*}
-
-If one does not give all the members in the \texttt{Instance}
-declaration, Coq enters the proof-mode and the user is asked to build
-inhabitants of the remaining fields, e.g.:
-
-\begin{coq_example*}
-Instance eq_bool : EqDec bool :=
-{ eqb x y := if x then y else negb y }.
-\end{coq_example*}
-\begin{coq_example}
-Proof. intros x y H.
-  destruct x ; destruct y ; (discriminate || reflexivity). 
-Defined.
-\end{coq_example}
-
-One has to take care that the transparency of every field is determined
-by the transparency of the \texttt{Instance} proof. One can use
-alternatively the \texttt{Program} \texttt{Instance} \comindex{Program Instance} variant which has
-richer facilities for dealing with obligations.
-
-\asection{Binding classes}
-
-Once a type class is declared, one can use it in class binders:
-\begin{coq_example}
-Definition neqb {A} {eqa : EqDec A} (x y : A) := negb (eqb x y).
-\end{coq_example}
-
-When one calls a class method, a constraint is generated that is
-satisfied only in contexts where the appropriate instances can be
-found. In the example above, a constraint \texttt{EqDec A} is generated and
-satisfied by \texttt{{eqa : EqDec A}}. In case no satisfying constraint can be
-found, an error is raised:
-
-\begin{coq_example}
-Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
-\end{coq_example}
-
-The algorithm used to solve constraints is a variant of the eauto tactic
-that does proof search with a set of lemmas (the instances). It will use
-local hypotheses as well as declared lemmas in the
-\texttt{typeclass\_instances} database. Hence the example can also be
-written:
-
-\begin{coq_example}
-Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y).
-\end{coq_example}
-
-However, the generalizing binders should be used instead as they have
-particular support for type classes:
-\begin{itemize}
-\item They automatically set the maximally implicit status for type
-  class arguments, making derived functions as easy to use as class
-  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.
-\item They also support implicit quantification on superclasses
-  (\S \ref{classes:superclasses})
-\end{itemize}
-
-Following the previous example, one can write:
-\begin{coq_example}
-Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).
-\end{coq_example}
-
-Here \texttt{A} is implicitly generalized, and the resulting function
-is equivalent to the one above.
-
-\asection{Parameterized Instances}
-
-One can declare parameterized instances as in \Haskell simply by giving
-the constraints as a binding context before the instance, e.g.:
-
-\begin{coq_example}
-Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) :=
-{ eqb x y := match x, y with
-  | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb)
-  end }.
-\end{coq_example}
-\begin{coq_eval}
-Admitted.
-\end{coq_eval}
-
-These instances are used just as well as lemmas in the instance hint database.
-
-\asection{Sections and contexts}
-\label{SectionContext}
-To ease the parametrization of developments by type classes, we provide
-a new way to introduce variables into section contexts, compatible with 
-the implicit argument mechanism. 
-The new command works similarly to the \texttt{Variables} vernacular
-(see \ref{Variable}), except it accepts any binding context as argument.
-For example:
-
-\begin{coq_example}
-Section EqDec_defs.
-  Context `{EA : EqDec A}.
-\end{coq_example}
-
-\begin{coq_example*}
-  Global Instance option_eqb : EqDec (option A) :=
-  { eqb x y := match x, y with
-    | Some x, Some y => eqb x y
-    | None, None => true
-    | _, _ => false
-    end }.
-\end{coq_example*}
-\begin{coq_eval}
-Proof.
-intros x y ; destruct x ; destruct y ; intros H ; 
-try discriminate ; try apply eqb_leibniz in H ;
-subst ; auto. 
-Defined.
-\end{coq_eval}
-
-\begin{coq_example}
-End EqDec_defs.
-About option_eqb.
-\end{coq_example}
-
-Here the \texttt{Global} modifier redeclares the instance at the end of 
-the section, once it has been generalized by the context variables it uses.
-
-\asection{Building hierarchies}
-
-\subsection{Superclasses}
-\label{classes:superclasses}
-One can also parameterize classes by other classes, generating a
-hierarchy of classes and superclasses. In the same way, we give the
-superclasses as a binding context:
-
-\begin{coq_example*}
-Class Ord `(E : EqDec A) :=
-  { le : A -> A -> bool }.
-\end{coq_example*}
-
-Contrary to \Haskell, we have no special syntax for superclasses, but
-this declaration is morally equivalent to:
-\begin{verbatim}
-Class `(E : EqDec A) => Ord A :=
-  { le : A -> A -> bool }.
-\end{verbatim}
-
-This declaration means that any instance of the \texttt{Ord} class must
-have an instance of \texttt{EqDec}. The parameters of the subclass contain
-at least all the parameters of its superclasses in their order of
-appearance (here \texttt{A} is the only one).
-As we have seen, \texttt{Ord} is encoded as a record type with two parameters:
-a type \texttt{A} and an \texttt{E} of type \texttt{EqDec A}. However, one can
-still use it as if it had a single parameter inside generalizing binders: the
-generalization of superclasses will be done automatically. 
-\begin{coq_example*}
-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:
-\begin{coq_example*}
-Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := 
-  andb (le x y) (neqb x y).
-\end{coq_example*}
-
-The \texttt{!} modifier switches the way a binder is parsed back to the
-regular interpretation of Coq. In particular, it uses the implicit
-arguments mechanism if available, as shown in the example.
-
-\subsection{Substructures}
-
-Substructures are components of a class which are instances of a class
-themselves. They often arise when using classes for logical properties,
-e.g.:
-
-\begin{coq_eval}
-Require Import Relations.
-\end{coq_eval}
-\begin{coq_example*}
-Class Reflexive (A : Type) (R : relation A) :=
-  reflexivity : forall x, R x x.
-Class Transitive (A : Type) (R : relation A) :=
-  transitivity : forall x y z, R x y -> R y z -> R x z.
-\end{coq_example*}
-
-This declares singleton classes for reflexive and transitive relations,
-(see \ref{SingletonClass} for an explanation).
-These may be used as part of other classes:
-
-\begin{coq_example*}
-Class PreOrder (A : Type) (R : relation A) :=
-{ PreOrder_Reflexive :> Reflexive A R ;
-  PreOrder_Transitive :> Transitive A R }.
-\end{coq_example*}
-
-The syntax \texttt{:>} indicates that each \texttt{PreOrder} can be seen
-as a \texttt{Reflexive} relation. So each time a reflexive relation is
-needed, a preorder can be used instead. This is very similar to the
-coercion mechanism of \texttt{Structure} declarations.
-The implementation simply declares each projection as an instance. 
-
-One can also declare existing objects or structure
-projections using the \texttt{Existing Instance} command to achieve the 
-same effect.
-
-\section{Summary of the commands
-\label{TypeClassCommands}}
-
-\subsection{\tt Class {\ident} {\binder$_1$ \ldots~\binder$_n$} 
-  : \sort := \{ field$_1$ ; \ldots ; field$_k$ \}.}
-\comindex{Class}
-\label{Class}
-
-The \texttt{Class} command is used to declare a type class with
-parameters {\binder$_1$} to {\binder$_n$} and fields {\tt field$_1$} to
-{\tt field$_k$}.
-
-\begin{Variants}
-\item \label{SingletonClass} {\tt Class {\ident} {\binder$_1$ \ldots \binder$_n$} 
-    : \sort := \ident$_1$ : \type$_1$.}
-  This variant declares a \emph{singleton} class whose only method is
-  {\tt \ident$_1$}. This singleton class is a so-called definitional
-  class, represented simply as a definition 
-  {\tt {\ident} \binder$_1$ \ldots \binder$_n$ := \type$_1$} and whose
-  instances are themselves objects of this type. Definitional classes
-  are not wrapped inside records, and the trivial projection of an
-  instance of such a class is convertible to the instance itself. This can
-  be useful to make instances of existing objects easily and to reduce 
-  proof size by not inserting useless projections. The class
-  constant itself is declared rigid during resolution so that the class 
-  abstraction is maintained.  
-
-\item \label{ExistingClass} {\tt Existing Class {\ident}.\comindex{Existing Class}}
-  This variant declares a class a posteriori from a constant or
-  inductive definition. No methods or instances are defined.
-\end{Variants}
-
-\subsection{\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} :
-  {Class} {t$_1$ \ldots t$_n$} [| \textit{priority}]
-  := \{ field$_1$ := b$_1$ ; \ldots ; field$_i$ := b$_i$ \}}
-\comindex{Instance}
-\label{Instance}
-
-The \texttt{Instance} command is used to declare a type class instance
-named {\ident} of the class \emph{Class} with parameters {t$_1$} to {t$_n$} and
-fields {\tt b$_1$} to {\tt b$_i$}, where each field must be a declared
-field of the class. Missing fields must be filled in interactive proof mode.
-
-An arbitrary context of the form {\tt \binder$_1$ \ldots \binder$_n$}
-can be put after the name of the instance and before the colon to
-declare a parameterized instance.
-An optional \textit{priority} can be declared, 0 being the highest
-priority as for auto hints.
-
-\begin{Variants}
-\item {\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} :
-    forall {\binder$_{n+1}$ \ldots \binder$_m$},
-    {Class} {t$_1$ \ldots t$_n$} [| \textit{priority}] := \term} 
-  This syntax is used for declaration of singleton class instances or
-  for directly giving an explicit term of type
-  {\tt forall {\binder$_{n+1}$ \ldots \binder$_m$}, {Class} {t$_1$ \ldots t$_n$}}.
-  One need not even mention the unique field name for singleton classes.
-
-\item {\tt Global Instance} One can use the \texttt{Global} modifier on
-  instances declared in a section so that their generalization is automatically
-  redeclared after the section is closed.
-
-\item {\tt Program Instance} \comindex{Program Instance}
-  Switches the type-checking to \Program~(chapter \ref{Program})
-  and uses the obligation mechanism to manage missing fields.
-
-\item {\tt Declare Instance} \comindex{Declare Instance}
-  In a {\tt Module Type}, this command states that a corresponding
-  concrete instance should exist in any implementation of this
-  {\tt Module Type}. This is similar to the distinction between
-  {\tt Parameter} vs. {\tt Definition}, or between {\tt Declare Module}
-  and {\tt Module}.
-
-\end{Variants}
-
-Besides the {\tt Class} and {\tt Instance} vernacular commands, there
-are a few other commands related to type classes.
-
-\subsection{\tt Existing Instance {\ident}}
-\comindex{Existing Instance}
-\label{ExistingInstance}
-
-This commands adds an arbitrary constant whose type ends with an applied
-type class to the instance database. It can be used for redeclaring
-instances at the end of sections, or declaring structure projections as
-instances. This is almost equivalent to {\tt Hint Resolve {\ident} :
-  typeclass\_instances}.
-
-\subsection{\tt Context {\binder$_1$ \ldots \binder$_n$}}
-\comindex{Context}
-\label{Context}
-
-Declares variables according to the given binding context, which might
-use implicit generalization (see \ref{SectionContext}).
-
-\subsection{\tt Typeclasses Transparent, Opaque {\ident$_1$ \ldots \ident$_n$}}
-\comindex{Typeclasses Transparent}
-\comindex{Typeclasses Opaque}
-\label{TypeclassesTransparency}
-
-This commands defines the transparency of {\ident$_1$ \ldots \ident$_n$} 
-during type class resolution. It is useful when some constants prevent some
-unifications and make resolution fail. It is also useful to declare
-constants which should never be unfolded during proof-search, like
-fixpoints or anything which does not look like an abbreviation. This can
-additionally speed up proof search as the typeclass map can be indexed
-by such rigid constants (see \ref{HintTransparency}).
-By default, all constants and local variables are considered transparent.
-One should take care not to make opaque any constant that is used to
-abbreviate a type, like {\tt relation A := A -> A -> Prop}.
-
-This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_instances}.
-
-\subsection{\tt Typeclasses eauto := [debug] [dfs | bfs] [\emph{depth}]}
-\comindex{Typeclasses eauto}
-\label{TypeclassesEauto}
-
-This commands allows to customize the type class resolution tactic,
-based on a variant of eauto. The flags semantics are:
-\begin{itemize}
-\item {\tt debug} In debug mode, the trace of successfully applied
-  tactics is printed.
-\item {\tt dfs, bfs} This sets the search strategy to depth-first search
-  (the default) or breadth-first search.
-\item {\emph{depth}} This sets the depth of the search (the default is 100).
-\end{itemize}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: