Imported Upstream version 8.3upstream/8.3

1 files changed, 2001 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
new file mode 100644
index 00000000..3e298867
--- /dev/null
+++ b/doc/refman/RefMan-tus.tex
@@ -0,0 +1,2001 @@
+%\documentclass[11pt]{article}
+%\usepackage{fullpage,euler}
+%\usepackage[latin1]{inputenc}
+%\begin{document}
+%\title{Writing ad-hoc Tactics in Coq}
+%\author{} 
+%\date{}
+%\maketitle
+%\tableofcontents
+%\clearpage
+
+\chapter[Writing ad-hoc Tactics in Coq]{Writing ad-hoc Tactics in Coq\label{WritingTactics}}
+
+\section{Introduction}
+
+\Coq\ is an open proof environment, in the sense that the collection of
+proof strategies offered by the system can be extended by the user.
+This feature has two important advantages. First, the user can develop
+his/her own ad-hoc proof procedures, customizing the system for a
+particular domain of application. Second, the repetitive and tedious
+aspects of the proofs can be abstracted away implementing new tactics
+for dealing with them. For example, this may be useful when a theorem
+needs several lemmas which are all proven in a similar but not exactly
+the same way. Let us illustrate this with an example.
+
+Consider the problem of deciding the equality of two booleans. The
+theorem establishing that this is always possible is state by 
+the following theorem:
+
+\begin{coq_example*}
+Theorem decideBool : (x,y:bool){x=y}+{~x=y}.
+\end{coq_example*}
+
+The proof proceeds by case analysis on both $x$ and $y$. This yields
+four cases to solve. The cases $x=y=\textsl{true}$ and
+$x=y=\textsl{false}$ are immediate by the reflexivity of equality.
+
+The other two cases follow by discrimination. The following script
+describes the proof:
+
+\begin{coq_example*}
+Destruct x.
+  Destruct y.
+    Left ; Reflexivity.
+    Right; Discriminate.
+  Destruct y.
+    Right; Discriminate.
+    Left ; Reflexivity.
+\end{coq_example*}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+Now, consider the theorem stating the same property but for the
+following enumerated type:
+
+\begin{coq_example*}
+Inductive Set Color := Blue:Color | White:Color | Red:Color.
+Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}.
+\end{coq_example*}
+
+This theorem can be proven in a very similar way, reasoning by case
+analysis on $c_1$ and $c_2$. Once more, each of the (now six) cases is
+solved either by reflexivity or by discrimination:
+
+\begin{coq_example*}
+Destruct c1. 
+  Destruct c2.
+    Left  ; Reflexivity.
+    Right ; Discriminate.
+    Right ; Discriminate.
+  Destruct c2.  
+    Right ; Discriminate.
+    Left  ; Reflexivity.
+    Right ; Discriminate.
+  Destruct c2.  
+    Right ; Discriminate.
+    Right ; Discriminate.
+    Left  ; Reflexivity.
+\end{coq_example*}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+If we face the same theorem for an enumerated datatype corresponding
+to the days of the week, it would still follow a similar pattern. In
+general, the general pattern for proving the property
+$(x,y:R)\{x=y\}+\{\neg x =y\}$ for an enumerated type $R$ proceeds as
+follow:
+\begin{enumerate}
+\item Analyze the cases for $x$. 
+\item For each of the sub-goals generated by the first step, analyze
+the cases for $y$.
+\item The remaining subgoals follow either by reflexivity or
+by discrimination.
+\end{enumerate}
+
+Let us describe how this general proof procedure can be introduced in
+\Coq.
+
+\section{Tactic Macros}
+
+The simplest way to introduce it is to define it as new a
+\textsl{tactic macro}, as follows:
+
+\begin{coq_example*}
+Tactic Definition DecideEq [$a $b] := 
+   [<:tactic:<Destruct $a;
+              Destruct $b;
+              (Left;Reflexivity) Orelse (Right;Discriminate)>>].
+\end{coq_example*}
+
+The general pattern of the proof is abstracted away using the
+tacticals ``\texttt{;}'' and \texttt{Orelse}, and introducing two
+parameters for the names of the arguments to be analyzed.
+
+Once defined, this tactic can be called like any other tactic, just
+supplying the list of terms corresponding to its real arguments. Let us
+revisit the proof of the former theorems using the new tactic
+\texttt{DecideEq}:
+
+\begin{coq_example*}
+Theorem decideBool : (x,y:bool){x=y}+{~x=y}.
+DecideEq x y.
+Defined.
+\end{coq_example*}
+\begin{coq_example*}
+Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}.
+DecideEq c1 c2.
+Defined.
+\end{coq_example*}
+
+In general, the command \texttt{Tactic Definition} associates a name
+to a parameterized tactic expression, built up from the tactics and
+tacticals that are already available. The general syntax rule for this
+command is the following:
+
+\begin{tabbing}
+\texttt{Tactic Definition} \textit{tactic-name} \= 
+\texttt{[}\$$id_1\ldots \$id_n$\texttt{]}\\
+\> := \texttt{[<:tactic:<} \textit{tactic-expression} \verb+>>]+
+\end{tabbing}
+
+This command provides a quick but also very primitive mechanism for
+introducing new tactics. It does not support recursive definitions,
+and the arguments of a tactic macro are restricted to term
+expressions.  Moreover, there is no static checking of the definition
+other than the syntactical one. Any error in the definition of the
+tactic ---for instance, a call to an undefined tactic--- will not be
+noticed until the tactic is called.
+
+%This command provides a very primitive mechanism for introducing new
+%tactics. The arguments of a tactic macro are restricted to term
+%expressions.  Hence, it is not possible to define higher order tactics
+%with this command. Also, there is no static checking of the definition
+%other than syntactical. If the tactic contain errors in its definition
+%--for instance, a call to an undefined tactic-- this will be noticed
+%during the tactic call.
+
+Let us illustrate the weakness of this way of introducing new tactics
+trying to extend our proof procedure to work on a larger class of
+inductive types.  Consider for example the decidability of equality
+for pairs of booleans and colors:
+
+\begin{coq_example*}
+Theorem decideBoolXColor : (p1,p2:bool*Color){p1=p2}+{~p1=p2}.
+\end{coq_example*}
+
+The proof still proceeds by a double case analysis, but now the
+constructors of the type take two arguments. Therefore, the sub-goals
+that can not be solved by discrimination need further considerations
+about the equality of such arguments:
+
+\begin{coq_example}
+  Destruct p1;
+    Destruct p2; Try (Right;Discriminate);Intros.
+\end{coq_example}
+
+The half of the disjunction to be chosen depends on whether or not
+$b=b_0$ and $c=c_0$. These equalities can be decided automatically
+using the previous lemmas about booleans and colors. If both
+equalities are satisfied, then it is sufficient to rewrite $b$ into
+$b_0$ and $c$ into $c_0$, so that the left half of the goal follows by
+reflexivity.  Otherwise, the right half follows by first contraposing
+the disequality, and then applying the invectiveness of the pairing
+constructor.
+
+As the cases associated to each argument of the pair are very similar,
+a tactic macro can be introduced to abstract this part of the proof:
+
+\begin{coq_example*}
+Hints Resolve decideBool decideColor.
+Tactic Definition SolveArg [$t1 $t2] := 
+ [<:tactic:<
+   ElimType {$t1=$t2}+{~$t1=$t2};
+   [(Intro equality;Rewrite equality;Clear equality) |
+    (Intro diseq; Right; Red; Intro absurd;
+     Apply diseq;Injection absurd;Trivial) |
+    Auto]>>].
+\end{coq_example*}
+
+This tactic is applied to each corresponding pair of arguments of the
+arguments, until the goal can be solved by reflexivity:
+
+\begin{coq_example*}
+SolveArg b b0;
+  SolveArg c c0;
+    Left; Reflexivity.
+Defined.
+\end{coq_example*}
+
+Therefore, a more general strategy for deciding the property 
+$(x,y:R)\{x=y\}+\{\neg x =y\}$ on $R$ can be sketched as follows:
+\begin{enumerate}
+\item Eliminate $x$ and then $y$.
+\item Try discrimination to solve those goals where $x$ and $y$ has
+been introduced by different constructors.
+\item If $x$ and $y$ have been introduced by the same constructor,
+then iterate the tactic \textsl{SolveArg} for each pair of
+arguments. 
+\item Finally, solve the left half of the goal by reflexivity.
+\end{enumerate}
+
+The implementation of this stronger proof strategy needs to perform a
+term decomposition, in order to extract the list of arguments of each
+constructor. It also requires the introduction of recursively defined
+tactics, so that the \textsl{SolveArg} can be iterated on the lists of
+arguments. These features are not supported by the \texttt{Tactic
+Definition} command. One possibility could be extended this command in
+order to introduce recursion, general parameter passing,
+pattern-matching, etc, but this would quickly lead us to introduce the
+whole \ocaml{} into \Coq\footnote{This is historically true. In fact,
+\ocaml{} is a direct descendent of ML, a functional programming language
+conceived language for programming the tactics of the theorem prover
+LCF.}.  Instead of doing this, we prefer to give to the user the
+possibility of writing his/her own tactics directly in \ocaml{}, and then
+to link them dynamically with \Coq's code. This requires a minimal
+knowledge about \Coq's implementation. The next section provides an
+overview of \Coq's architecture.
+
+%It is important to point out that the introduction of a new tactic
+%never endangers the correction of the theorems proven in the extended
+%system. In order to understand why, let us introduce briefly the system
+%architecture.
+
+\section{An Overview of \Coq's Architecture}
+
+The implementation of \Coq\ is based on eight \textsl{logical
+modules}. By ``module'' we mean here a logical piece of code having a
+conceptual unity, that may concern several \ocaml{} files. By the sake of
+organization, all the \ocaml{} files concerning a logical module are
+grouped altogether into the same sub-directory. The eight modules
+are:
+
+\begin{tabular}{lll}
+1. & The logical framework           & (directory \texttt{src/generic})\\
+2. &  The language of constructions  & (directory \texttt{src/constr})\\
+3. &  The type-checker               & (directory \texttt{src/typing})\\
+4. &  The proof engine               & (directory \texttt{src/proofs})\\
+5. &  The language of basic tactics  & (directory \texttt{src/tactics})\\
+6. &  The vernacular interpreter     & (directory \texttt{src/env})\\
+7. &  The parser and the pretty-printer  & (directory \texttt{src/parsing})\\
+8. &  The standard library           & (directory \texttt{src/lib})
+\end{tabular}
+
+\vspace{1em}
+
+The following sections briefly present each of the modules above.
+This presentation is not intended to be a complete description of \Coq's
+implementation, but rather a guideline to be read before taking a look
+at the sources. For each of the modules, we also present some of its
+most important functions, which are sufficient to implement a large
+class of tactics.
+
+
+\subsection[The Logical Framework]{The Logical Framework\label{LogicalFramework}}
+
+At the very heart of \Coq there is a generic untyped language for
+expressing abstractions, applications and global constants. This
+language is used as a meta-language for expressing the terms of the
+Calculus of Inductive Constructions. General operations on terms like
+collecting the free variables of an expression, substituting a term for
+a free variable, etc, are expressed in this language.
+
+The meta-language \texttt{'op term} of terms has seven main
+constructors:
+\begin{itemize}
+\item $(\texttt{VAR}\;id)$, a reference to a global identifier called  $id$;
+\item $(\texttt{Rel}\;n)$, a bound variable, whose binder is the $nth$
+      binder up in the term;
+\item $\texttt{DLAM}\;(x,t)$, a deBruijn's binder on the term $t$;
+\item $\texttt{DLAMV}\;(x,vt)$, a deBruijn's binder on all the terms of 
+      the vector $vt$;
+\item $(\texttt{DOP0}\;op)$, a unary operator $op$;
+\item $\texttt{DOP2}\;(op,t_1,t_2)$, the application of a binary
+operator $op$ to the terms $t_1$ and $t_2$;
+\item $\texttt{DOPN} (op,vt)$, the application of an n-ary operator $op$ to the
+vector of terms $vt$.
+\end{itemize}
+
+In this meta-language, bound variables are represented using the
+so-called deBrujin's indexes. In this representation, an occurrence of
+a bound variable is denoted by an integer, meaning the number of
+binders that must be traversed to reach its own
+binder\footnote{Actually, $(\texttt{Rel}\;n)$ means that $(n-1)$ binders
+have to be traversed, since indexes are represented by strictly
+positive integers.}. On the other hand, constants are referred by its
+name, as usual. For example, if $A$ is a variable of the current
+section, then the lambda abstraction $[x:A]x$ of the Calculus of
+Constructions is represented in the meta-language by the term:
+
+\begin{displaymath}
+(DOP2 (Lambda,(Var\;A),DLAM (x,(Rel\;1)))
+\end{displaymath}
+
+In this term, $Lambda$ is a binary operator.  Its first argument
+correspond to the type $A$ of the bound variable, while the second is
+a body of the abstraction, where $x$ is bound.  The name $x$ is just kept
+to pretty-print the occurrences of the bound variable.
+
+%Similarly, the product
+%$(A:Prop)A$ of the Calculus of Constructions is represented by the
+%term:
+%\begin{displaumath}
+%DOP2 (Prod, DOP0 (Sort (Prop Null)), DLAM (Name \#A, Rel 1))
+%\end{displaymath}
+
+The following functions perform some of the most frequent operations
+on the terms of the meta-language:
+\begin{description}
+\fun{val Generic.subst1 : 'op term -> 'op term -> 'op term}
+    {$(\texttt{subst1}\;t_1\;t_2)$ substitutes $t_1$ for 
+      $\texttt{(Rel}\;1)$ in $t_2$.}
+\fun{val Generic.occur\_var : identifier -> 'op term -> bool}
+    {Returns true when the given identifier appears in the term,
+    and false otherwise.}
+\fun{val Generic.eq\_term : 'op term -> 'op term -> bool}
+    {Implements $\alpha$-equality for terms.}  
+\fun{val Generic.dependent : 'op term -> 'op term -> bool}
+    {Returns true if the first term is a sub-term of the second.}
+%\fun{val Generic.subst\_var : identifier -> 'op term -> 'op term}
+%    { $(\texttt{subst\_var}\;id\;t)$ substitutes the deBruijn's index
+%     associated to $id$ to every occurrence of the term
+%    $(\texttt{VAR}\;id)$ in $t$.}
+\end{description}
+
+\subsubsection{Identifiers, names and sections paths.} 
+
+Three different kinds of names are used in the meta-language. They are
+all defined in the \ocaml{} file \texttt{Names}.
+
+\paragraph{Identifiers.}  The simplest kind of names are
+\textsl{identifiers}. An identifier is a string possibly indexed by an
+integer. They are used to represent names that are not unique, like
+for example the name of a variable in the scope of a section.  The
+following operations can be used for handling identifiers:
+
+\begin{description}
+\fun{val Names.make\_ident : string -> int -> identifier}
+    {The value $(\texttt{make\_ident}\;x\;i)$ creates the
+    identifier $x_i$. If $i=-1$, then the identifier has
+    is created with no index at all.}
+\fun{val Names.repr\_ident : identifier -> string * int}
+    {The inverse operation of \texttt{make\_ident}: 
+     it yields the string and the index of the identifier.}
+\fun{val Names.lift\_ident : identifier -> identifier}
+    {Increases the index of the identifier by one.}
+\fun{val Names.next\_ident\_away : \\
+\qquad identifier -> identifier list -> identifier}
+    {\\ Generates a new identifier with the same root string than the
+    given one, but with a new index, different from all the indexes of
+    a given list of identifiers.} 
+\fun{val Names.id\_of\_string : string ->
+    identifier} 
+    {Creates an identifier from a string.}  
+\fun{val  Names.string\_of\_id : identifier -> string} 
+    {The inverse operation: transforms an identifier into a string}
+\end{description}
+
+\paragraph{Names.} A \textsl{name} is either an identifier or the 
+special name \texttt{Anonymous}. Names are used as arguments of
+binders, in order to pretty print bound variables.
+The following operations can be used for handling names:
+
+\begin{description}
+\fun{val Names.Name: identifier -> Name}
+    {Constructs a name from  an identifier.}
+\fun{val Names.Anonymous : Name}
+    {Constructs a special, anonymous identifier, like the variable abstracted 
+     in the term $[\_:A]0$.}
+\fun{val
+     Names.next\_name\_away\_with\_default : \\ \qquad
+          string->name->identifier list->identifier}
+{\\ If the name is not anonymous, then this function generates a new
+    identifier different from all the ones in a given list. Otherwise, it
+    generates an identifier from the given string.}
+\end{description}
+
+\paragraph[Section paths.]{Section paths.\label{SectionPaths}}
+A \textsl{section-path} is a global name to refer to an object without
+ambiguity.  It can be seen as a sort of filename, where open sections
+play the role of directories. Each section path is formed by three
+components: a \textsl{directory} (the list of open sections); a
+\textsl{basename} (the identifier for the object); and a \textsl{kind}
+(either CCI for the terms of the Calculus of Constructions, FW for the
+the terms of $F_\omega$, or OBJ for other objects). For example, the
+name of the following constant:
+\begin{verbatim}
+     Section A.
+     Section B.
+     Section C.
+     Definition zero := O.
+\end{verbatim}
+
+is internally represented by the section path:
+
+$$\underbrace{\mathtt{\#A\#B\#C}}_{\mbox{dirpath}}
+\underbrace{\mathtt{\tt \#zero}}_{\mbox{basename}}
+\underbrace{\mathtt{\tt .cci}_{\;}}_{\mbox{kind}}$$
+
+When one of the sections is closed, a new constant is created with an
+updated section-path,a nd the old one is no longer reachable.  In our
+example, after closing the section \texttt{C}, the new section-path
+for the constant {\tt zero} becomes:
+\begin{center}
+\texttt{ \#A\#B\#zero.cci}
+\end{center}
+
+The following operations can be used to handle section paths:
+
+\begin{description}
+\fun{val Names.string\_of\_path : section\_path -> string}
+    {Transforms the section path into a string.}
+\fun{val Names.path\_of\_string : string -> section\_path}
+    {Parses a string an returns the corresponding section path.}
+\fun{val Names.basename : section\_path -> identifier}
+    {Provides the basename of a section path}
+\fun{val Names.dirpath : section\_path -> string list}
+    {Provides the directory of a section path}
+\fun{val Names.kind\_of\_path : section\_path -> path\_kind}
+    {Provides the kind of a section path}
+\end{description}
+
+\subsubsection{Signatures} 
+
+A \textsl{signature} is a mapping associating different informations
+to identifiers (for example, its type, its definition, etc). The
+following operations could be useful for working with signatures:
+
+\begin{description}
+\fun{val Names.ids\_of\_sign  : 'a signature -> identifier list}
+    {Gets the list of identifiers of the signature.}
+\fun{val Names.vals\_of\_sign : 'a signature -> 'a list}
+    {Gets the list of values associated to the identifiers of the signature.}
+\fun{val Names.lookup\_glob1 : \\ \qquad
+identifier -> 'a signature -> (identifier *
+    'a)}
+    {\\ Gets the value associated to a given identifier of the signature.}
+\end{description}
+
+
+\subsection{The Terms of the Calculus of Constructions}
+
+The language of the Calculus of Inductive Constructions described in
+Chapter \ref{Cic} is implemented on the top of the logical framework,
+instantiating the parameter $op$ of the meta-language with a
+particular set of operators.  In the implementation this language is
+called \texttt{constr}, the language of constructions.
+
+% The only difference
+%with respect to the one described in Section \ref{} is that the terms
+%of \texttt{constr} may contain \textsl{existential variables}. An
+%existential variable is a place holder representing a part of the term
+%that is still to be constructed. Such ``open terms'' are necessary
+%when building proofs interactively.
+
+\subsubsection{Building Constructions}
+
+The user does not need to know the choices made to represent
+\texttt{constr} in the meta-language. They are abstracted away by the
+following constructor functions:
+
+\begin{description}
+\fun{val Term.mkRel          : int -> constr}
+    {$(\texttt{mkRel}\;n)$ represents deBrujin's index $n$.}
+
+\fun{val Term.mkVar : identifier -> constr} 
+    {$(\texttt{mkVar}\;id)$
+    represents a global identifier named $id$, like a variable
+    inside the scope of a section, or a hypothesis in a proof}.
+
+\fun{val Term.mkExistential : constr} 
+   {\texttt{mkExistential} represents an implicit sub-term, like the question
+    marks in the term \texttt{(pair ? ? O true)}.}
+
+%\fun{val Term.mkMeta         : int -> constr}
+%    {$(\texttt{mkMeta}\;n)$ represents an existential variable, whose
+%     name is the integer $n$.}
+
+\fun{val Term.mkProp         : constr}
+    {$\texttt{mkProp}$ represents the sort \textsl{Prop}.}
+
+\fun{val Term.mkSet          : constr}
+    {$\texttt{mkSet}$ represents the sort \textsl{Set}.}
+
+\fun{val Term.mkType         : Impuniv.universe -> constr}
+    {$(\texttt{mkType}\;u)$ represents the term
+    $\textsl{Type}(u)$. The universe $u$ is represented as a 
+    section path indexed by an integer. }
+
+\fun{val Term.mkConst : section\_path -> constr array -> constr}
+    {$(\texttt{mkConst}\;c\;v)$ represents a constant whose name is
+    $c$. The body of the constant is stored in a global table,
+    accessible through the name of the constant. The array of terms
+    $v$ corresponds to the variables of the environment appearing in
+    the body of the constant when it was defined. For instance, a
+    constant defined in the section \textsl{Foo} containing the
+    variable $A$, and whose body is $[x:Prop\ra Prop](x\;A)$ is
+    represented inside the scope of the section by
+    $(\texttt{mkConst}\;\texttt{\#foo\#f.cci}\;[| \texttt{mkVAR}\;A
+    |])$.  Once the section is closed, the constant is represented by
+    the term $(\texttt{mkConst}\;\#f.cci\;[| |])$, and its body
+    becomes $[A:Prop][x:Prop\ra Prop](x\;A)$}.
+
+\fun{val Term.mkMutInd : section\_path -> int -> constr array ->constr}
+    {$(\texttt{mkMutInd}\;c\;i)$ represents the $ith$ type
+    (starting from zero) of the block of mutually dependent
+    (co)inductive types, whose first type is $c$.  Similarly to the
+    case of constants, the array of terms represents the current
+    environment of the (co)inductive type. The definition of the type
+    (its arity, its constructors, whether it is inductive or co-inductive, etc.)
+    is stored in a global hash table, accessible through the name of 
+    the type.}
+
+\fun{val Term.mkMutConstruct : \\ \qquad section\_path -> int -> int -> constr array
+    ->constr} {\\ $(\texttt{mkMutConstruct}\;c\;i\;j)$ represents the
+    $jth$ constructor of the $ith$ type of the block of mutually
+    dependent (co)inductive types whose first type is $c$. The array
+    of terms represents the current environment of the (co)inductive
+    type.}
+
+\fun{val Term.mkCast : constr -> constr -> constr}
+    {$(\texttt{mkCast}\;t\;T)$ represents the annotated term $t::T$ in
+    \Coq's syntax.}  
+
+\fun{val Term.mkProd : name ->constr ->constr -> constr}
+    {$(\texttt{mkProd}\;x\;A\;B)$ represents the product $(x:A)B$.
+     The free ocurrences of $x$ in $B$ are represented by deBrujin's
+     indexes.}
+
+\fun{val Term.mkNamedProd : identifier -> constr -> constr -> constr}
+    {$(\texttt{produit}\;x\;A\;B)$ represents the product $(x:A)B$,
+     but the bound occurrences of $x$ in $B$ are denoted by 
+     the identifier $(\texttt{mkVar}\;x)$. The function automatically 
+     changes each occurrences of this identifier into the corresponding 
+     deBrujin's index.}
+
+\fun{val Term.mkArrow : constr -> constr -> constr}
+    {$(\texttt{arrow}\;A\;B)$ represents the type $(A\rightarrow B)$.}
+
+\fun{val Term.mkLambda       : name -> constr -> constr -> constr}
+    {$(\texttt{mkLambda}\;x\;A\;b)$ represents the lambda abstraction 
+     $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by deBrujin's
+     indexes.}
+
+\fun{val Term.mkNamedLambda : identifier -> constr -> constr -> constr}
+    {$(\texttt{lambda}\;x\;A\;b)$ represents the lambda abstraction 
+     $[x:A]b$, but the bound occurrences of $x$ in $B$ are denoted by 
+     the identifier $(\texttt{mkVar}\;x)$. }
+
+\fun{val Term.mkAppLA        : constr array -> constr}
+    {$(\texttt{mkAppLA}\;t\;[|t_1\ldots t_n|])$ represents the application
+    $(t\;t_1\;\ldots t_n)$.}
+
+\fun{val Term.mkMutCaseA : \\ \qquad
+    case\_info -> constr ->constr
+    ->constr array -> constr} 
+    {\\ $(\texttt{mkMutCaseA}\;r\;P\;m\;[|f_1\ldots f_n|])$
+    represents the term \Case{P}{m}{f_1\ldots f_n}. The first argument
+    $r$ is either \texttt{None} or $\texttt{Some}\;(c,i)$, where the
+    pair $(c,i)$ refers to the inductive type that $m$ belongs to.}
+
+\fun{val Term.mkFix :  \\ \qquad
+int array->int->constr array->name
+    list->constr array->constr}
+    {\\ $(\texttt{mkFix}\;[|k_1\ldots k_n |]\;i\;[|A_1\ldots
+    A_n|]\;[|f_1\ldots f_n|]\;[|t_1\ldots t_n|])$ represents the term
+    $\Fix{f_i}{f_1/k_1:A_1:=t_1 \ldots f_n/k_n:A_n:=t_n}$}
+
+\fun{val Term.mkCoFix  : \\ \qquad
+    int -> constr array -> name list ->
+    constr array -> constr}
+    {\\ $(\texttt{mkCoFix}\;i\;[|A_1\ldots
+    A_n|]\;[|f_1\ldots f_n|]\;[|t_1\ldots t_n|])$ represents the term
+    $\CoFix{f_i}{f_1:A_1:=t_1 \ldots f_n:A_n:=t_n}$. There are no
+    decreasing indexes in this case.}
+\end{description}
+
+\subsubsection{Decomposing Constructions}
+
+Each of the construction functions above has its corresponding
+(partial) destruction function, whose name is obtained changing the
+prefix \texttt{mk} by \texttt{dest}. In addition to these functions, a
+concrete datatype \texttt{kindOfTerm} can be used to do pattern
+matching on terms without dealing with their internal representation
+in the meta-language. This concrete datatype is described in the \ocaml{}
+file \texttt{term.mli}. The following function transforms a construction
+into an element of type \texttt{kindOfTerm}:
+
+\begin{description}
+\fun{val Term.kind\_of\_term : constr -> kindOfTerm}
+    {Destructs a term of the language \texttt{constr},
+yielding the direct components of the term. Hence, in order to do 
+pattern matching on an object $c$ of \texttt{constr}, it is sufficient
+to do pattern matching on the value $(\texttt{kind\_of\_term}\;c)$.}
+\end{description}
+
+Part of the information associated to the constants is stored in 
+global tables. The following functions give access to such 
+information:
+
+\begin{description}
+\fun{val Termenv.constant\_value    : constr -> constr}
+    {If the term denotes a constant, projects the body of a constant}
+\fun{Termenv.constant\_type     : constr -> constr}
+    {If the term denotes a constant, projects the type of the constant}
+\fun{val mind\_arity        : constr -> constr}
+    {If the term denotes an inductive type, projects its arity (i.e.,
+     the type of the inductive type).}
+\fun{val Termenv.mis\_is\_finite    : mind\_specif -> bool}
+    {Determines whether a recursive type is inductive or co-inductive.}
+\fun{val Termenv.mind\_nparams : constr -> int}
+    {If the term denotes an inductive type, projects the number of 
+     its general parameters.}
+\fun{val Termenv.mind\_is\_recursive : constr -> bool}
+    {If the term denotes an inductive type, 
+     determines if the type has at least one recursive constructor. }
+\fun{val Termenv.mind\_recargs : constr -> recarg list array array}
+    {If the term denotes an inductive type, returns an array $v$ such 
+     that the nth element of $v.(i).(j)$ is
+    \texttt{Mrec} if the $nth$ argument of the $jth$ constructor of
+    the $ith$ type is recursive, and \texttt{Norec} if it is not.}.
+\end{description}
+
+\subsection[The Type Checker]{The Type Checker\label{TypeChecker}}
+
+The third logical module is the type checker. It concentrates two main
+tasks concerning the language of constructions.
+
+On one hand, it contains the type inference and type-checking
+functions.  The type inference function takes a term
+$a$ and a signature $\Gamma$, and yields a term $A$ such that
+$\Gamma \vdash a:A$.  The type-checking function takes two terms $a$
+and $A$ and a signature $\Gamma$, and determines whether or not
+$\Gamma \vdash a:A$.
+
+On the other hand, this module is in charge of the compilation of
+\Coq's abstract syntax trees into the language \texttt{constr} of
+constructions. This compilation seeks to eliminate all the ambiguities
+contained in \Coq's abstract syntax, restoring the information
+necessary to type-check it.  It concerns at least the following steps:
+\begin{enumerate}
+\item Compiling the pattern-matching expressions containing 
+constructor patterns, wild-cards, etc, into terms that only
+use the primitive \textsl{Case} described in Chapter \ref{Cic}
+\item Restoring type coercions and synthesizing the implicit arguments
+(the one denoted by question marks in
+{\Coq} syntax: see Section~\ref{Coercions}).
+\item Transforming the named bound variables into deBrujin's indexes.
+\item Classifying the global names into the different classes of
+constants (defined constants, constructors, inductive types, etc).
+\end{enumerate}
+
+\subsection{The Proof Engine}
+
+The fourth stage of \Coq's implementation is the \textsl{proof engine}:
+the interactive machine for constructing proofs. The aim of the proof
+engine is to construct a top-down derivation or \textsl{proof tree},
+by the application of \textsl{tactics}. A proof tree has the following
+general structure:\\
+
+\begin{displaymath}
+\frac{\Gamma \vdash ? = t(?_1,\ldots?_n) : G}
+     {\hspace{3ex}\frac{\displaystyle \Gamma_1 \vdash ?_1 = t_1(\ldots) : G_1}
+         {\stackrel{\vdots}{\displaystyle {\Gamma_{i_1} \vdash ?_{i_1} 
+           : G_{i_1}}}}(tac_1)
+      \;\;\;\;\;\;\;\;\;
+      \frac{\displaystyle \Gamma_n \vdash ?_n = t_n(\ldots) : G_n}
+         {\displaystyle \stackrel{\vdots}{\displaystyle {\Gamma_{i_m} \vdash ?_{i_m} :
+     G_{i_m}}}}(tac_n)} (tac)    
+\end{displaymath}
+
+
+\noindent Each node of the tree is called a \textsl{goal}. A goal
+is a record type containing the following three fields:
+\begin{enumerate}
+\item the conclusion $G$ to be proven;
+\item a typing signature $\Gamma$ for the free variables in $G$;
+\item if the goal is an internal node of the proof tree, the
+definition $t(?_1,\ldots?_n)$ of an \textsl{existential variable}
+(i.e. a possible undefined constant) $?$ of type $G$ in terms of the
+existential variables of the children sub-goals. If the node is a
+leaf, the existential variable maybe still undefined.
+\end{enumerate}
+
+Once all the existential variables have been defined the derivation is
+completed, and a construction can be generated from the proof tree,
+replacing each of the existential variables by its definition.  This
+is exactly what happens when one of the commands
+\texttt{Qed}, \texttt{Save} or \texttt{Defined} is invoked
+(see Section~\ref{Qed}). The saved theorem becomes a defined constant,
+whose body is the proof object generated.
+
+\paragraph{Important:} Before being added to the
+context, the proof object is type-checked, in order to verify that it is
+actually an object of the expected type $G$.  Hence, the correctness
+of the proof actually does not depend on the tactics applied to
+generate it or the machinery of the proof engine, but only on the
+type-checker. In other words, extending the system with a potentially
+bugged new tactic never endangers the consistency of the system.
+
+\subsubsection[What is a Tactic?]{What is a Tactic?\label{WhatIsATactic}}
+%Let us now explain what is a tactic, and how the user can introduce
+%new ones. 
+
+From an operational point of view, the current state of the proof
+engine is given by the mapping $emap$ from existential variables into
+goals, plus a pointer to one of the leaf goals $g$.  Such a pointer
+indicates where the proof tree will be refined by the application of a
+\textsl{tactic}. A tactic is a function from the current state
+$(g,emap)$ of the proof engine into a pair $(l,val)$. The first
+component of this pair is the list of children sub-goals $g_1,\ldots
+g_n$ of $g$ to be yielded by the tactic. The second one is a
+\textsl{validation function}. Once the proof trees $\pi_1,\ldots
+\pi_n$ for $g_1,\ldots g_n$ have been completed, this validation
+function must yield a proof tree $(val\;\pi_1,\ldots \pi_n)$ deriving
+$g$.
+
+Tactics can be classified into \textsl{primitive} ones and
+\textsl{defined} ones. Primitive tactics correspond to the five basic
+operations of the proof engine:
+
+\begin{enumerate}
+\item Introducing a universally quantified variable into the local
+context of the goal.
+\item Defining an undefined existential variable 
+\item Changing the conclusion of the goal for another
+--definitionally equal-- term.
+\item Changing the type of a variable in the local context for another
+definitionally equal term.
+\item Erasing a variable from the local context.
+\end{enumerate}
+
+\textsl{Defined} tactics are tactics constructed by combining these
+primitive operations.  Defined tactics are registered in a hash table,
+so that they can be introduced dynamically. In order to define such a
+tactic table, it is necessary to fix what a \textsl{possible argument}
+of a tactic may be. The type \texttt{tactic\_arg} of the possible
+arguments for tactics is a union type including:
+\begin{itemize}
+\item quoted strings;
+\item integers;
+\item identifiers;
+\item lists of identifiers;
+\item plain terms, represented by its abstract syntax tree;
+\item well-typed terms, represented by a construction;
+\item a substitution for bound variables, like the
+substitution in the tactic \\$\texttt{Apply}\;t\;\texttt{with}\;x:=t_1\ldots
+x_n:=t_n$, (see Section~\ref{apply});
+\item a reduction expression, denoting the reduction strategy to be
+followed.
+\end{itemize}
+Therefore, for each function $tac:a \rightarrow tactic$ implementing a
+defined tactic, an associated dynamic tactic $tacargs\_tac:
+\texttt{tactic\_arg}\;list \rightarrow tactic$ calling $tac$ must be
+written. The aim of the auxiliary function $tacargs\_tac$ is to inject
+the arguments of the tactic $tac$ into the type of possible arguments
+for a tactic.
+
+The following function can be used for registering and calling a
+defined tactic:
+
+\begin{description}
+\fun{val Tacmach.add\_tactic : \\ \qquad
+string -> (tactic\_arg list ->tactic) -> unit}
+    {\\ Registers a dynamic tactic with the given string as access index.}
+\fun{val Tacinterp.vernac\_tactic : string*tactic\_arg list -> tactic}
+    {Interprets a defined tactic given by its entry in the
+     tactics table with a particular list of possible arguments.}
+\fun{val Tacinterp.vernac\_interp        : CoqAst.t -> tactic}
+    {Interprets a tactic expression formed combining \Coq's tactics and
+          tacticals, and described by its abstract syntax tree.}
+\end{description}
+
+When programming a new tactic that calls an already defined tactic
+$tac$, we have the choice between using the \ocaml{} function
+implementing $tac$, or calling the tactic interpreter with the name
+and arguments for interpreting $tac$. In the first case, a tactic call
+will left the trace of the whole implementation of $tac$ in the proof
+tree. In the second, the implementation of $tac$ will be hidden, and
+only an invocation of $tac$ will be recalled (cf. the example of
+Section \ref{ACompleteExample}.  The following combinators can be used
+to hide the implementation of a tactic:
+
+\begin{verbatim}
+type 'a hiding_combinator = string -> ('a -> tactic) -> ('a -> tactic)
+val Tacmach.hide_atomic_tactic  : string -> tactic -> tactic
+val Tacmach.hide_constr_tactic  : constr          hiding_combinator
+val Tacmach.hide_constrl_tactic : (constr list)   hiding_combinator
+val Tacmach.hide_numarg_tactic  : int             hiding_combinator
+val Tacmach.hide_ident_tactic   : identifier      hiding_combinator
+val Tacmach.hide_identl_tactic  : identifier      hiding_combinator
+val Tacmach.hide_string_tactic  : string          hiding_combinator
+val Tacmach.hide_bindl_tactic   : substitution    hiding_combinator
+val Tacmach.hide_cbindl_tactic  : 
+          (constr * substitution) hiding_combinator
+\end{verbatim}
+
+These functions first register the tactic by a side effect, and then
+yield a function calling the interpreter with the registered name and
+the right injection into the type of possible arguments.
+
+\subsection{Tactics and Tacticals Provided by \Coq}
+
+The fifth logical module is the library of tacticals and basic tactics
+provided by \Coq. This library is distributed into the directories
+\texttt{tactics} and \texttt{src/tactics}. The former contains those
+basic tactics that make use of the types contained in the basic state
+of \Coq. For example, inversion or rewriting tactics are in the
+directory \texttt{tactics}, since they make use of the propositional
+equality type.  Those tactics which are independent from the context
+--like for example \texttt{Cut}, \texttt{Intros}, etc-- are defined in
+the directory \texttt{src/tactics}. This latter directory also
+contains some useful tools for programming new tactics, referred in 
+Section \ref{SomeUsefulToolsforWrittingTactics}.
+
+In practice, it is very unusual that the list of sub-goals and the
+validation function of the tactic must be explicitly constructed by
+the user. In most of the cases, the implementation of a new tactic
+consists in supplying the appropriate arguments to the basic tactics
+and tacticals.
+
+\subsubsection{Basic Tactics}
+
+The file \texttt{Tactics} contain the implementation of the basic
+tactics provided by \Coq. The following tactics are some of the most
+used ones:
+
+\begin{verbatim}
+val Tactics.intro           : tactic
+val Tactics.assumption      : tactic
+val Tactics.clear           : identifier list -> tactic
+val Tactics.apply           : constr -> constr substitution -> tactic
+val Tactics.one_constructor : int -> constr substitution -> tactic
+val Tactics.simplest_elim   : constr -> tactic
+val Tactics.elimType        : constr -> tactic
+val Tactics.simplest_case   : constr -> tactic
+val Tactics.caseType        : constr -> tactic
+val Tactics.cut             : constr -> tactic
+val Tactics.reduce          : redexpr -> tactic
+val Tactics.exact           : constr -> tactic
+val Auto.auto               : int option -> tactic
+val Auto.trivial            : tactic
+\end{verbatim}
+
+The functions hiding the implementation of these tactics are defined
+in the module \texttt{Hiddentac}. Their names are prefixed by ``h\_''.
+
+\subsubsection[Tacticals]{Tacticals\label{OcamlTacticals}}
+
+The following tacticals can be used to combine already existing
+tactics:
+
+\begin{description}
+\fun{val Tacticals.tclIDTAC : tactic}
+    {The identity tactic: it leaves the goal as it is.}
+
+\fun{val Tacticals.tclORELSE : tactic -> tactic -> tactic}
+    {Tries the first tactic and in case of failure applies the second one.}
+
+\fun{val Tacticals.tclTHEN : tactic -> tactic -> tactic}
+  {Applies the first tactic and then the second one to each generated subgoal.}
+
+\fun{val Tacticals.tclTHENS : tactic -> tactic list -> tactic}
+    {Applies a tactic, and then applies each tactic of the tactic list to the
+     corresponding generated subgoal.}
+
+\fun{val Tacticals.tclTHENL : tactic -> tactic -> tactic}
+    {Applies the first tactic, and then applies the second one to the last
+     generated subgoal.}
+
+\fun{val Tacticals.tclREPEAT : tactic -> tactic}
+    {If the given tactic succeeds in producing a subgoal, then it
+     is recursively applied to each generated subgoal, 
+     and so on until it fails. }
+
+\fun{val Tacticals.tclFIRST : tactic list -> tactic}
+    {Tries the tactics of the given list one by one, until one of them
+     succeeds.}
+
+\fun{val Tacticals.tclTRY : tactic -> tactic}
+    {Tries the given tactic and in case of failure applies the {\tt
+    tclIDTAC} tactical to the original goal.}
+
+\fun{val Tacticals.tclDO : int -> tactic -> tactic}
+    {Applies the tactic a given number of times.}
+
+\fun{val Tacticals.tclFAIL : tactic}
+    {The always failing tactic: it raises a {\tt UserError} exception.}
+
+\fun{val Tacticals.tclPROGRESS  : tactic -> tactic}
+    {Applies the given tactic to the current goal and fails if the 
+     tactic leaves the goal unchanged}
+
+\fun{val Tacticals.tclNTH\_HYP :  int -> (constr -> tactic) -> tactic}
+    {Applies a tactic to the nth hypothesis of the local context.
+     The last hypothesis introduced correspond to the integer 1.}
+
+\fun{val Tacticals.tclLAST\_HYP :  (constr -> tactic) -> tactic}
+    {Applies a tactic to the last hypothesis introduced.}
+
+\fun{val Tacticals.tclCOMPLETE : tactic -> tactic}
+    {Applies a tactic and fails if the tactic did not solve completely the
+      goal}
+
+\fun{val Tacticals.tclMAP : ('a -> tactic) -> 'a list -> tactic}
+    {Applied to the function \texttt{f} and the list \texttt{[x\_1;
+        ... ; x\_n]}, this tactical applies the tactic
+      \texttt{tclTHEN (f x1) (tclTHEN (f x2) ... ))))}}
+    
+\fun{val Tacicals.tclIF : (goal sigma -> bool) -> tactic -> tactic -> tactic}
+    {If the condition holds, apply the first tactic; otherwise,
+      apply the second one}
+
+\end{description}
+
+
+\subsection{The Vernacular Interpreter}
+
+The sixth logical module of the implementation corresponds to the
+interpreter of the vernacular phrases of \Coq. These phrases may be
+expressions from the \gallina{} language (definitions), general
+directives (setting commands) or tactics to be applied by the proof
+engine. 
+
+\subsection[The Parser and the Pretty-Printer]{The Parser and the Pretty-Printer\label{PrettyPrinter}}
+
+The last logical module is the parser and pretty printer of \Coq,
+which is the interface between the vernacular interpreter and the
+user. They translate the chains of characters entered at the input
+into abstract syntax trees, and vice versa. Abstract syntax trees are
+represented by labeled n-ary trees, and its type is called
+\texttt{CoqAst.t}.  For instance, the abstract syntax tree associated
+to the term $[x:A]x$ is:
+
+\begin{displaymath}
+\texttt{Node}
+ ((0,6), "LAMBDA",
+  [\texttt{Nvar}~((3, 4),"A");~\texttt{Slam}~((0,6),~Some~"x",~\texttt{Nvar}~((5,6),"x"))])
+\end{displaymath}
+
+The numbers correspond to \textsl{locations}, used to point to some
+input line and character positions in the error messages. As it was
+already explained in Section \ref{TypeChecker}, this term is then
+translated into a construction term in order to be typed.
+
+The parser of \Coq\ is implemented using \camlpppp. The lexer and the data
+used by \camlpppp\ to generate the parser lay in the directory
+\texttt{src/parsing}.  This directory also contains \Coq's
+pretty-printer. The printing rules lay in the directory
+\texttt{src/syntax}.  The different entries of the grammar are
+described in the module \texttt{Pcoq.Entry}.  Let us present here two
+important functions of this logical module:
+
+\begin{description}
+\fun{val Pcoq.parse\_string : 'a Grammar.Entry.e -> string -> 'a}
+    {Parses a given string, trying to recognize a phrase
+     corresponding to some entry in the grammar. If it succeeds,
+     it yields a value associated to the grammar entry. For example,
+     applied to the entry \texttt{Pcoq.Command.command}, this function
+    parses a term of \Coq's language, and yields a value of type 
+    \texttt{CoqAst.t}. When applied to the entry
+    \texttt{Pcoq.Vernac.vernac}, it parses a vernacular command and
+    returns the corresponding Ast.}
+\fun{val gentermpr       : \\ \qquad 
+path\_kind -> constr assumptions -> constr -> std\_ppcmds}
+    {\\ Pretty-prints a well-typed term of certain kind (cf. Section
+    \ref{SectionPaths}) under its context of typing assumption.}
+\fun{val gentacpr        : CoqAst.t -> std\_ppcmds}
+    {Pretty-prints a given abstract syntax tree representing a tactic
+     expression.}
+\end{description}
+
+\subsection{The General Library}
+
+In addition to the ones laying in the standard library of \ocaml{},
+several useful modules about lists, arrays, sets, mappings, balanced
+trees, and other frequently used data structures can be found in the
+directory \texttt{lib}. Before writing a new one, check if it is not
+already there!
+
+\subsubsection{The module \texttt{Std}}
+This module in the directory \texttt{src/lib/util} is opened by almost 
+all modules of \Coq{}. Among other things, it contains a definition of 
+the different kinds of errors used in \Coq{} :
+
+\begin{description}
+\fun{exception UserError of string * std\_ppcmds}
+    {This is the class of ``users exceptions''. Such errors arise when 
+      the user attempts to do something illegal, for example \texttt{Intro}
+      when the current goal conclusion is not a product.}
+
+\fun{val Std.error : string -> 'a}
+    {For simple error messages}
+\fun{val Std.errorlabstrm : string -> std\_ppcmds -> 'a}
+    {See Section~\ref{PrettyPrinter} : this can be used if the user
+      want to display a term or build a complex error message}
+
+\fun{exception Anomaly of string * std\_ppcmds}
+    {This for reporting bugs or things that should not
+      happen. The tacticals \texttt{tclTRY} and
+      \texttt{tclTRY} described in Section~\ref{OcamlTacticals} catch the
+      exceptions of type \texttt{UserError}, but they don't catch the
+      anomalies. So, in your code, don't raise any anomaly, unless you
+      know what you are doing. We also recommend to avoid constructs
+      such as \texttt{try ... with \_ -> ...} : such constructs can trap 
+      an anomaly and make the debugging process harder.}
+
+\fun{val Std.anomaly : string -> 'a}{}
+\fun{val Std.anomalylabstrm : string -> std\_ppcmds -> 'a}{}
+\end{description}
+
+\section{The tactic writer mini-HOWTO}
+
+\subsection{How to add a vernacular command}
+
+The command to register a vernacular command can be found
+in module \texttt{Vernacinterp}:
+
+\begin{verbatim}
+val vinterp_add : string * (vernac_arg list -> unit -> unit) -> unit;;
+\end{verbatim}
+
+The first argument is the name, the second argument is a function that
+parses the arguments and returns a function of type
+\texttt{unit}$\rightarrow$\texttt{unit} that do the job.
+
+In this section we will show how to add a vernacular command
+\texttt{CheckCheck} that print a type of a term and the type of its
+type.
+
+File \texttt{dcheck.ml}:
+
+\begin{verbatim}
+open Vernacinterp;;
+open Trad;;
+let _ = 
+  vinterp_add 
+   ("DblCheck",
+    function [VARG_COMMAND com] ->
+       (fun () -> 
+          let evmap = Evd.mt_evd () 
+          and sign = Termenv.initial_sign () in
+           let {vAL=c;tYP=t;kIND=k} = 
+                 fconstruct_with_univ evmap sign com in
+             Pp.mSGNL [< Printer.prterm c; 'sTR ":"; 
+                       Printer.prterm t; 'sTR ":"; 
+                       Printer.prterm k >] )
+      | _ -> bad_vernac_args "DblCheck")
+;;
+\end{verbatim}
+
+Like for a new tactic, a new syntax entry must be created.
+
+File \texttt{DCheck.v}:
+
+\begin{verbatim}
+Declare ML Module "dcheck.ml".
+
+Grammar vernac vernac := 
+  dblcheck [ "CheckCheck" comarg($c) ] -> [(DblCheck $c)].
+\end{verbatim}
+
+We are now able to test our new command:
+
+\begin{verbatim}
+Coq < Require DCheck.
+Coq < CheckCheck O.
+O:nat:Set
+\end{verbatim}
+
+Most Coq vernacular commands are registered in the module 
+  \verb+src/env/vernacentries.ml+. One can see more examples here.
+
+\subsection{How to keep a hashtable synchronous with the reset mechanism}
+
+This is far more tricky. Some vernacular commands modify some
+sort of state (for example by adding something in a hashtable). One
+wants that \texttt{Reset} has the expected behavior with this
+commands.
+
+\Coq{} provides a general mechanism to do that. \Coq{} environments
+contains objects of three kinds: CCI, FW and OBJ. CCI and FW are for
+constants of the calculus. OBJ is a dynamically extensible datatype
+that contains sections, tactic definitions, hints for auto, and so
+on. 
+
+The simplest example of use of such a mechanism is in file
+\verb+src/proofs/macros.ml+ (which implements the \texttt{Tactic
+  Definition} command). Tactic macros are stored in the imperative
+hashtable \texttt{mactab}. There are two functions freeze and unfreeze
+to make a copy of the table and to restore the state of table from the
+copy. Then this table is declared using \texttt{Library.declare\_summary}.
+
+What does \Coq{} with that ? \Coq{} defines synchronization points.
+At each synchronisation point, the declared tables are frozen (that
+is, a copy of this tables is stored).
+
+When \texttt{Reset }$i$ is called, \Coq{} goes back to the first
+synchronisation point that is above $i$ and ``replays'' all objects
+between that point 
+and $i$. It will re-declare constants, re-open section, etc.
+
+So we need to declare a new type of objects, TACTIC-MACRO-DATA. To
+``replay'' on object of that type is to add the corresponding tactic
+macro to \texttt{mactab}
+
+So, now, we can say that \texttt{mactab} is synchronous with the Reset
+mechanism$^{\mathrm{TM}}$.
+
+Notice that this works for hash tables but also for a single integer
+(the Undo stack size, modified by the \texttt{Set Undo} command, for
+example).
+
+\subsection{The right way to access to Coq constants from your ML code}
+
+With their long names, Coq constants are stored using:
+
+\begin{itemize}
+\item a section path
+\item an identifier
+\end{itemize}
+
+The identifier is exactly the identifier that is used in \Coq{} to
+denote the constant; the section path can be known using the
+\texttt{Locate} command:
+
+\begin{coq_example}
+  Locate S.
+  Locate nat.
+  Locate eq.
+\end{coq_example}
+
+Now it is easy to get a constant by its name and section path:
+
+
+\begin{verbatim}
+let constant sp id = 
+  Machops.global_reference (Names.gLOB (Termenv.initial_sign ())) 
+    (Names.path_of_string sp) (Names.id_of_string id);;
+\end{verbatim}
+
+
+The only issue is that if one cannot put:
+
+
+\begin{verbatim}
+let coq_S = constant "#Datatypes#nat.cci" "S";;
+\end{verbatim}
+
+
+in his tactic's code. That is because this sentence is evaluated
+\emph{before} the module \texttt{Datatypes} is loaded. The solution is
+to use the lazy evaluation of \ocaml{}:
+
+
+\begin{verbatim}
+let coq_S = lazy (constant "#Datatypes#nat.cci" "S");;
+
+... (Lazy.force coq_S) ...
+\end{verbatim}
+
+
+Be sure to call always Lazy.force behind a closure -- i.e. inside a
+function body or behind the \texttt{lazy} keyword.
+
+One can see examples of that technique in the source code of \Coq{},
+for example 
+\verb+plugins/omega/coq_omega.ml+.
+
+\section[Some Useful Tools for Writing Tactics]{Some Useful Tools for Writing Tactics\label{SomeUsefulToolsforWrittingTactics}}
+When the implementation of a tactic is not a straightforward
+combination of tactics and tacticals, the module \texttt{Tacmach}
+provides several useful functions for handling goals, calling the
+type-checker, parsing terms, etc. This module is intended to be 
+the interface of the proof engine for the user.
+
+\begin{description}
+\fun{val Tacmach.pf\_hyps               : goal sigma -> constr signature}
+    {Projects the local typing context $\Gamma$ from a given goal $\Gamma\vdash ?:G$.} 
+\fun{val pf\_concl              : goal sigma -> constr}
+    {Projects the conclusion $G$ from a given goal $\Gamma\vdash ?:G$.}
+\fun{val Tacmach.pf\_nth\_hyp            : goal sigma -> int -> identifier *
+    constr}
+    {Projects the $ith$ typing constraint $x_i:A_i$ from the local
+     context of the given goal.}
+\fun{val Tacmach.pf\_fexecute           : goal sigma -> constr -> judgement}
+    {Given a goal whose local context is $\Gamma$ and a term $a$, this
+     function infers a type $A$ and a kind $K$ such that the judgement
+     $a:A:K$ is valid under $\Gamma$, or raises an exception if there
+     is no such judgement. A judgement is just a record type containing
+     the three terms $a$, $A$ and $K$.}
+\fun{val Tacmach.pf\_infexecute : \\
+     \qquad
+goal sigma -> constr -> judgement * information}
+    {\\ In addition to the typing judgement, this function also extracts 
+     the $F_{\omega}$ program underlying the term.}
+\fun{val Tacmach.pf\_type\_of            : goal sigma -> constr -> constr}
+    {Infers a term $A$ such that $\Gamma\vdash a:A$ for a given term
+    $a$, where $\Gamma$ is the local typing context of the goal.}
+\fun{val Tacmach.pf\_check\_type         : goal sigma -> constr -> constr -> bool}
+    {This function yields a type $A$ if the two given terms $a$ and $A$  verify $\Gamma\vdash
+     a:A$ in the local typing context $\Gamma$ of the goal. Otherwise,
+    it raises an exception.}
+\fun{val Tacmach.pf\_constr\_of\_com      : goal sigma -> CoqAst.t -> constr}
+    {Transforms an abstract syntax tree into a well-typed term of the
+    language of constructions. Raises an exception if the term cannot
+    be typed.}
+\fun{val Tacmach.pf\_constr\_of\_com\_sort : goal sigma -> CoqAst.t -> constr}
+    {Transforms an abstract syntax tree representing a type into
+    a well-typed term of the language of constructions. Raises an
+    exception if the term cannot be typed.}
+\fun{val Tacmach.pf\_parse\_const        : goal sigma -> string -> constr}
+    {Constructs the constant whose name is the given string.}
+\fun{val
+Tacmach.pf\_reduction\_of\_redexp  : \\
+         \qquad goal sigma -> red\_expr -> constr -> constr}
+    {\\ Applies a certain kind of reduction function, specified by an
+     element of the type red\_expr.}
+\fun{val Tacmach.pf\_conv\_x      : goal sigma -> constr -> constr -> bool}
+    {Test whether  two given terms are definitionally equal.}
+\end{description}
+
+\subsection[Patterns]{Patterns\label{Patterns}}
+
+The \ocaml{} file \texttt{Pattern} provides a quick way for describing a
+term pattern and performing second-order, binding-preserving, matching
+on it. Patterns are described using an extension of \Coq's concrete
+syntax, where the second-order meta-variables of the pattern are
+denoted by indexed question marks. 
+
+Patterns may depend on constants, and therefore only to make have
+sense when certain theories have been loaded. For this reason, they
+are stored with a \textsl{module-marker}, telling us which modules
+have to be open in order to use the pattern. The following functions
+can be used to store and retrieve patterns form the pattern table:
+
+\begin{description}
+\fun{val Pattern.make\_module\_marker : string list -> module\_mark}
+    {Constructs a module marker from a list of module names.}
+\fun{val Pattern.put\_pat : module\_mark -> string -> marked\_term}
+    {Constructs a pattern from a parseable string containing holes
+     and a module marker.}
+\fun{val Pattern.somatches    : constr ->   marked\_term-> bool}
+    {Tests if a term matches a pattern.} 
+\fun{val dest\_somatch : constr -> marked\_term -> constr list}
+    {If the term matches the pattern, yields the list of sub-terms
+     matching the occurrences of the pattern variables (ordered from
+     left to right). Raises a \texttt{UserError} exception if the term
+     does not match the pattern.} 
+\fun{val Pattern.soinstance : marked\_term -> constr list -> constr} 
+    {Substitutes each hole in the pattern 
+     by the corresponding term of the given the list.}
+\end{description}
+
+\paragraph{Warning:} Sometimes, a \Coq\ term may have invisible
+sub-terms that the matching functions are nevertheless sensible to.
+For example, the \Coq\ term $(?_1,?_2)$ is actually a shorthand for
+the expression $(\texttt{pair}\;?\;?\;?_1\;?_2)$.
+Hence, matching this term pattern 
+with the term $(\texttt{true},\texttt{O})$ actually yields the list
+$[?;?;\texttt{true};\texttt{O}]$ as result (and \textbf{not}
+$[\texttt{true};\texttt{O}]$, as could be expected).
+
+\subsection{Patterns on Inductive Definitions}
+
+The module \texttt{Pattern} also includes some functions for testing
+if the definition of an inductive type satisfies certain
+properties. Such functions may be used to perform pattern matching
+independently from the name given to the inductive type and the
+universe it inhabits.  They yield the value $(\texttt{Some}\;r::l)$ if
+the input term reduces into an application of an inductive type $r$ to
+a list of terms $l$, and the definition of $r$ satisfies certain
+conditions. Otherwise, they yield the value \texttt{None}.
+
+\begin{description}
+\fun{val Pattern.match\_with\_non\_recursive\_type : constr list option}
+    {Tests if the inductive type $r$ has no recursive constructors}
+\fun{val Pattern.match\_with\_disjunction : constr list option}
+    {Tests if the inductive type $r$ is a non-recursive type
+     such that all its constructors have a single argument.}
+\fun{val Pattern.match\_with\_conjunction : constr list option}
+    {Tests if the inductive type $r$ is a non-recursive type
+     with a unique constructor.}
+\fun{val Pattern.match\_with\_empty\_type  : constr list option}
+    {Tests if the inductive type $r$ has no constructors at all}
+\fun{val Pattern.match\_with\_equation    : constr list option}
+    {Tests if the inductive type $r$ has a single constructor
+     expressing the property of reflexivity for some type. For
+     example, the types $a=b$, $A\mbox{==}B$ and $A\mbox{===}B$ satisfy
+     this predicate.}
+\end{description}
+
+\subsection{Elimination Tacticals}
+
+It is frequently the case that the subgoals generated by an
+elimination can all be solved in a similar way, possibly parametrized
+on some information about each case, like for example:
+\begin{itemize}
+\item the inductive type of the object being eliminated;
+\item its arguments (if it is an inductive predicate);
+\item the branch number;
+\item the predicate to be proven;
+\item the number of assumptions to be introduced by the case
+\item the signature of the branch, i.e., for each argument of
+the branch whether it is recursive or not.
+\end{itemize}
+
+The following tacticals can be useful to deal with such situations.
+They  
+
+\begin{description}
+\fun{val Elim.simple\_elimination\_then : \\ \qquad
+(branch\_args -> tactic) -> constr -> tactic}
+    {\\ Performs the default elimination on the last argument, and then
+     tries to solve the generated subgoals using a given parametrized
+     tactic. The type branch\_args is a record type containing all 
+     information mentioned above.}
+\fun{val Elim.simple\_case\_then : \\ \qquad
+(branch\_args -> tactic) -> constr -> tactic}
+    {\\ Similarly, but it performs case analysis instead of induction.}
+\end{description}
+
+\section[A Complete Example]{A Complete Example\label{ACompleteExample}}
+
+In order to illustrate the implementation of a new tactic, let us come
+back to the problem of deciding the equality of two elements of an
+inductive type.
+
+\subsection{Preliminaries}
+
+Let us call \texttt{newtactic} the directory that will contain the
+implementation of the new tactic. In this directory will lay two
+files: a file \texttt{eqdecide.ml}, containing the \ocaml{} sources that
+implements the tactic, and a \Coq\ file \texttt{Eqdecide.v}, containing
+its associated grammar rules and the commands to generate a module
+that can be loaded dynamically from \Coq's toplevel. 
+
+To compile our project, we will create a \texttt{Makefile} with the
+command \texttt{do\_Makefile} (see Section~\ref{Makefile}) :
+
+\begin{quotation}
+  \texttt{do\_Makefile eqdecide.ml EqDecide.v > Makefile}\\
+  \texttt{touch .depend}\\
+  \texttt{make depend}
+\end{quotation}
+
+We must have kept the sources of \Coq{} somewhere and to set an
+environment variable \texttt{COQTOP} that points to that directory.
+
+\subsection{Implementing the Tactic}
+
+The file \texttt{eqdecide.ml} contains the implementation of the
+tactic in \ocaml{}. Let us recall the main steps of the proof strategy
+for deciding the proposition $(x,y:R)\{x=y\}+\{\neg x=y\}$ on the
+inductive type $R$:
+\begin{enumerate}
+\item Eliminate $x$ and then $y$.
+\item Try discrimination to solve those goals where $x$ and $y$ has
+been introduced by different constructors.
+\item If $x$ and $y$ have been introduced by the same constructor,
+      then analyze one by one the corresponding pairs of arguments.
+      If they are equal, rewrite one into the other. If they are
+      not, derive a contradiction from the invectiveness of the
+      constructor.
+\item Once all the arguments have been rewritten, solve the left half
+of the goal by reflexivity.
+\end{enumerate}
+
+In the sequel we implement these steps one by one. We start opening
+the modules necessary for the implementation of the tactic:
+
+\begin{verbatim}
+open Names
+open Term
+open Tactics
+open Tacticals
+open Hiddentac
+open Equality
+open Auto
+open Pattern
+open Names
+open Termenv
+open Std
+open Proof_trees
+open Tacmach
+\end{verbatim}
+
+The first step of the procedure can be straightforwardly implemented as
+follows:
+
+\begin{verbatim}
+let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))));;
+\end{verbatim}
+
+\begin{verbatim}
+let mkBranches = 
+        (tclTHEN  intro 
+        (tclTHEN (tclLAST_HYP h_simplest_elim)
+        (tclTHEN  clear_last
+        (tclTHEN  intros 
+        (tclTHEN (tclLAST_HYP h_simplest_case)
+        (tclTHEN  clear_last
+                  intros))))));;
+\end{verbatim}
+
+Notice the use of the tactical \texttt{tclLAST\_HYP}, which avoids to
+give a (potentially clashing) name to the quantified variables of the
+goal when they are introduced.
+
+The second step of the procedure is implemented by the following
+tactic:
+
+\begin{verbatim}
+let solveRightBranch  = (tclTHEN simplest_right discrConcl);;
+\end{verbatim}
+
+In order to illustrate how the implementation of a tactic can be 
+hidden, let us do it with the tactic above:
+
+\begin{verbatim}
+let h_solveRightBranch =
+    hide_atomic_tactic "solveRightBranch" solveRightBranch
+;;
+\end{verbatim}
+
+As it was already mentioned in Section \ref{WhatIsATactic}, the
+combinator \texttt{hide\_atomic\_tactic} first registers the tactic
+\texttt{solveRightBranch} in the table, and returns a tactic which
+calls the interpreter with the used to register it. Hence, when the
+tactical \texttt{Info} is used, our tactic will just inform that
+\texttt{solveRightBranch} was applied, omitting all the details
+corresponding to \texttt{simplest\_right} and \texttt{discrConcl}.
+
+
+
+The third step requires some auxiliary functions for constructing the
+type $\{c_1=c_2\}+\{\neg c_1=c_2\}$ for a given inductive type $R$ and
+two constructions $c_1$ and $c_2$, and for generalizing this type over
+$c_1$ and $c_2$:
+
+\begin{verbatim}
+let mmk         = make_module_marker ["#Logic.obj";"#Specif.obj"];;
+let eqpat       = put_pat mmk "eq";;                 
+let sumboolpat  = put_pat mmk "sumbool";;             
+let notpat      = put_pat mmk "not";;   
+let eq          = get_pat eqpat;;
+let sumbool     = get_pat sumboolpat;;
+let not         = get_pat notpat;;
+
+let mkDecideEqGoal rectype c1 c2 g = 
+     let equality    = mkAppL [eq;rectype;c1;c2] in
+     let disequality = mkAppL [not;equality]
+     in  mkAppL [sumbool;equality;disequality]
+;;
+let mkGenDecideEqGoal rectype g = 
+      let hypnames = ids_of_sign (pf_hyps g) in 
+      let xname    = next_ident_away (id_of_string "x") hypnames
+      and yname    = next_ident_away (id_of_string "y") hypnames
+      in  (mkNamedProd xname rectype 
+           (mkNamedProd yname rectype 
+            (mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g)))
+;;
+\end{verbatim}
+
+The tactic will depend on the \Coq modules \texttt{Logic} and
+\texttt{Specif}, since we use the constants corresponding to
+propositional equality (\texttt{eq}), computational disjunction
+(\texttt{sumbool}), and logical negation (\texttt{not}), defined in
+that modules. This is specified creating the module maker
+\texttt{mmk} (see Section~\ref{Patterns}).
+
+The third step of the procedure can be divided into three sub-steps.
+Assume that both $x$ and $y$ have been introduced by the same
+constructor.  For each corresponding pair of arguments of that
+constructor, we have to consider whether they are equal or not.  If
+they are equal, the following tactic is applied to rewrite one into
+the other:
+
+\begin{verbatim}
+let eqCase  tac = 
+         (tclTHEN intro  
+         (tclTHEN (tclLAST_HYP h_rewriteLR)
+         (tclTHEN clear_last 
+                  tac)))
+;;
+\end{verbatim}
+
+
+If they are not equal, then the goal is contraposed and a
+contradiction is reached form the invectiveness of the constructor:
+
+\begin{verbatim}
+let diseqCase = 
+    let diseq  = (id_of_string "diseq") in
+    let absurd = (id_of_string "absurd")
+    in (tclTHEN (intro_using diseq)
+       (tclTHEN  h_simplest_right
+       (tclTHEN  red_in_concl
+       (tclTHEN  (intro_using absurd)
+       (tclTHEN  (h_simplest_apply (mkVar diseq))
+       (tclTHEN  (h_injHyp absurd)
+                  trivial ))))))
+;;
+\end{verbatim}
+
+In the tactic above we have chosen to name the hypotheses because
+they have to be applied later on. This introduces a potential risk
+of name clashing if the context already contains other hypotheses 
+also named ``diseq'' or ``absurd''.
+
+We are now ready to implement the tactic \textsl{SolveArg}.  Given the
+two arguments $a_1$ and $a_2$ of the constructor, this tactic cuts the
+goal with the proposition $\{a_1=a_2\}+\{\neg a_1=a_2\}$, and then
+applies the tactics above to each of the generated cases. If the
+disjunction cannot be solved automatically, it remains as a sub-goal
+to be proven.
+
+\begin{verbatim}
+let solveArg a1 a2 tac  g = 
+     let rectype = pf_type_of g a1 in
+     let decide  = mkDecideEqGoal rectype a1 a2 g
+     in  (tclTHENS  (h_elimType decide) 
+                      [(eqCase tac);diseqCase;default_auto]) g
+;;
+\end{verbatim}
+
+The following tactic implements the third and fourth steps of the
+proof procedure:
+
+\begin{verbatim}
+let conclpatt = put_pat mmk "{<?1>?2=?3}+{?4}"
+;;
+let solveLeftBranch rectype g = 
+      let (_::(lhs::(rhs::_))) = 
+               try (dest_somatch (pf_concl g) conclpatt) 
+               with UserError ("somatch",_)-> error "Unexpected conclusion!" in
+      let nparams   = mind_nparams rectype   in
+      let getargs l = snd (chop_list nparams (snd (decomp_app l))) in
+      let rargs   = getargs rhs
+      and largs   = getargs lhs
+      in  List.fold_right2 
+             solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g
+;;
+\end{verbatim}
+
+Notice the use of a pattern to decompose the goal and obtain the
+inductive type and the left and right hand sides of the equality. A
+certain number of arguments correspond to the general parameters of
+the type, and must be skipped over. Once the corresponding list of
+arguments \texttt{rargs} and \texttt{largs} have been obtained, the
+tactic \texttt{solveArg} is iterated on them, leaving a disjunction
+whose left half can be solved by reflexivity.
+
+The following tactic joints together the three steps of the 
+proof procedure:
+
+\begin{verbatim}
+let initialpatt = put_pat mmk "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}"
+;;
+let decideGralEquality g = 
+  let (typ::_) = try (dest_somatch (pf_concl g) initialpatt)
+                 with UserError ("somatch",_) -> 
+                        error "The goal does not have the expected form" in
+  let headtyp = hd_app (pf_compute g typ) in
+  let rectype = match (kind_of_term  headtyp) with
+                 IsMutInd _ -> headtyp 
+               | _          -> error ("This decision procedure only"
+                                      " works for inductive objects") 
+  in (tclTHEN   mkBranches 
+     (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g
+;;
+;;
+\end{verbatim}
+
+The tactic above can be specialized in two different ways: either to
+decide a particular instance $\{c_1=c_2\}+\{\neg c_1=c_2\}$ of the
+universal quantification; or to eliminate this property and obtain two
+subgoals containing the hypotheses $c_1=c_2$ and $\neg c_1=c_2$
+respectively.
+
+\begin{verbatim}
+let decideGralEquality = 
+  (tclTHEN mkBranches (tclORELSE h_solveRightBranch solveLeftBranch))
+;;
+let decideEquality c1 c2 g = 
+     let rectype = pf_type_of g c1 in
+     let decide  = mkGenDecideEqGoal rectype g
+     in  (tclTHENS (cut decide) [default_auto;decideGralEquality]) g
+;;
+let compare c1 c2 g = 
+     let rectype = pf_type_of g c1 in
+     let decide  = mkDecideEqGoal rectype c1 c2 g
+     in  (tclTHENS (cut decide) 
+                [(tclTHEN  intro 
+                 (tclTHEN (tclLAST_HYP simplest_case)
+                          clear_last));
+                  decideEquality c1 c2]) g
+;;
+\end{verbatim}
+
+Next, for each of the tactics that will have an entry in the grammar
+we construct the associated dynamic one to be registered in the table
+of tactics. This function can be used to overload a tactic name with
+several similar tactics.  For example, the tactic proving the general
+decidability property and the one proving a particular instance for
+two terms can be grouped together with the following convention: if
+the user provides two terms as arguments, then the specialized tactic
+is used; if no argument is provided then the general tactic is invoked.
+
+\begin{verbatim}
+let dyn_decideEquality  args g =
+      match args with 
+       [(COMMAND com1);(COMMAND com2)]  -> 
+          let c1 = pf_constr_of_com g com1
+          and c2 = pf_constr_of_com g com2
+          in  decideEquality c1 c2 g 
+     | [] ->  decideGralEquality g
+     | _  ->  error "Invalid arguments for dynamic tactic"
+;;
+add_tactic "DecideEquality" dyn_decideEquality
+;;
+
+let dyn_compare args g =
+      match args with 
+       [(COMMAND com1);(COMMAND com2)]  -> 
+          let c1 = pf_constr_of_com g com1
+          and c2 = pf_constr_of_com g com2
+          in  compare c1 c2 g
+     | _  ->  error "Invalid arguments for dynamic tactic"
+;; 
+add_tactic "Compare" tacargs_compare
+;;
+\end{verbatim}
+
+This completes the implementation of the tactic. We turn now to the
+\Coq file \texttt{Eqdecide.v}.
+
+
+\subsection{The Grammar Rules}
+
+Associated to the implementation of the tactic there is a \Coq\ file
+containing the grammar and pretty-printing rules for the new tactic,
+and the commands to generate an object module that can be then loaded
+dynamically during a \Coq\ session. In order to generate an ML module,
+the \Coq\ file must contain a
+\texttt{Declare ML module} command for all the \ocaml{} files concerning
+the implementation of the tactic --in our case there is only one file,
+the file \texttt{eqdecide.ml}: 
+
+\begin{verbatim}
+Declare ML Module "eqdecide".
+\end{verbatim}
+
+The following grammar and pretty-printing rules are
+self-explanatory. We refer the reader to the Section \ref{Grammar} for
+the details:
+
+\begin{verbatim}
+Grammar tactic simple_tactic :=
+  EqDecideRuleG1 
+       [ "Decide"  "Equality" comarg($com1)  comarg($com2)] -> 
+       [(DecideEquality $com1 $com2)]
+| EqDecideRuleG2 
+       [ "Decide" "Equality"  ] -> 
+       [(DecideEquality)]
+| CompareRule 
+       [ "Compare" comarg($com1) comarg($com2)] -> 
+       [(Compare $com1 $com2)].
+
+Syntax tactic level 0:
+  EqDecideRulePP1 
+       [(DecideEquality)]   -> 
+       ["Decide" "Equality"]
+| EqDecideRulePP2 
+       [(DecideEquality $com1 $com2)]   -> 
+       ["Decide" "Equality" $com1 $com2]
+| ComparePP 
+       [(Compare $com1 $com2)] -> 
+       ["Compare" $com1 $com2].
+\end{verbatim}
+
+
+\paragraph{Important:} The names used to label the abstract syntax tree 
+in the grammar rules ---in this case ``DecideEquality'' and
+``Compare''--- must be the same as the name used to register the
+tactic in the tactics table. This is what makes the links between the
+input entered by the user and the tactic executed by the interpreter.
+
+\subsection{Loading the Tactic}
+
+Once the module \texttt{EqDecide.v} has been compiled, the tactic can
+be dynamically loaded using the \texttt{Require} command. 
+
+\begin{coq_example}
+Require EqDecide.
+Goal (x,y:nat){x=y}+{~x=y}.
+Decide Equality.
+\end{coq_example}
+
+The implementation of the tactic can be accessed through the
+tactical \texttt{Info}:
+\begin{coq_example}
+Undo.
+Info Decide Equality.
+\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+Remark that the task performed by the tactic \texttt{solveRightBranch}
+is not displayed, since we have chosen to hide its implementation.
+
+\section[Testing and Debugging your Tactic]{Testing and Debugging your Tactic\label{test-and-debug}}
+
+When your tactic does not behave as expected, it is possible to trace
+it dynamically from \Coq. In order to do this, you have first to leave
+the toplevel of \Coq, and come back to the \ocaml{} interpreter. This can
+be done using the command \texttt{Drop} (see Section~\ref{Drop}). Once
+in the \ocaml{} toplevel, load the file \texttt{tactics/include.ml}.
+This file installs several pretty printers for proof trees, goals,
+terms, abstract syntax trees, names, etc.  It also contains the
+function \texttt{go:unit -> unit} that enables to go back to \Coq's
+toplevel. 
+
+The modules \texttt{Tacmach} and \texttt{Pfedit} contain some basic
+functions for extracting information from the state of the proof
+engine. Such functions can be used to debug your tactic if
+necessary. Let us mention here some of them:
+
+\begin{description}
+\fun{val get\_pftreestate         : unit -> pftreestate}
+    {Projects the current state of the proof engine.}
+\fun{val proof\_of\_pftreestate    : pftreestate -> proof}
+    {Projects the current state of the proof tree. A pretty-printer 
+      displays it in a readable form.  }
+\fun{val top\_goal\_of\_pftreestate : pftreestate -> goal sigma}
+    {Projects the goal and the existential variables mapping from
+     the current state of the proof engine.} 
+\fun{val nth\_goal\_of\_pftreestate : int -> pftreestate -> goal sigma}
+    {Projects the goal and mapping corresponding to the $nth$ subgoal
+     that remains to be proven}
+\fun{val traverse                : int -> pftreestate -> pftreestate}
+    {Yields the children of the node that the current state of the 
+     proof engine points to.}
+\fun{val solve\_nth\_pftreestate   : \\ \qquad
+int -> tactic -> pftreestate ->  pftreestate}
+     {\\ Provides the new state of the proof engine obtained applying 
+      a given tactic to some unproven sub-goal.}
+\end{description}
+
+Finally, the traditional \ocaml{} debugging tools like the directives
+\texttt{trace} and \texttt{untrace} can be used to follow the
+execution of your functions. Frequently, a better solution is to use
+the \ocaml{} debugger, see Chapter \ref{Utilities}.
+
+\section[Concrete syntax for ML tactic and vernacular command]{Concrete syntax for ML tactic and vernacular command\label{Notations-for-ML-command}}
+
+\subsection{The general case}
+
+The standard way to bind an ML-written tactic or vernacular command to
+a concrete {\Coq} syntax is to use the
+\verb=TACTIC EXTEND= and \verb=VERNAC COMMAND EXTEND= macros.
+
+These macros can be used in any {\ocaml} file defining a (new) ML tactic
+or vernacular command. They are expanded into pure {\ocaml} code by
+the {\camlpppp} preprocessor of {\ocaml}. Concretely, files that use
+these macros need to be compiled by giving to {\tt ocamlc} the option 
+
+\verb=-pp "camlp4o -I $(COQTOP)/parsing grammar.cma pa_extend.cmo"=
+
+\noindent which is the default for every file compiled by means of a Makefile
+generated by {\tt coq\_makefile} (see Chapter~\ref{Addoc-coqc}). So,
+just do \verb=make= in this latter case.
+
+The syntax of the macros is given on figure
+\ref{EXTEND-syntax}. They can be used at any place of an {\ocaml}
+files where an ML sentence (called \verb=str_item= in the {\tt ocamlc}
+parser) is expected. For each rule, the left-hand-side describes the
+grammar production and the right-hand-side its interpretation which
+must be an {\ocaml} expression. Each grammar production starts with
+the concrete name of the tactic or command in {\Coq} and is followed
+by arguments, possibly separated by terminal symbols or words.
+Here is an example:
+
+\begin{verbatim}
+TACTIC EXTEND Replace
+  [ "replace" constr(c1) "with" constr(c2) ] -> [ replace c1 c2 ]
+END
+\end{verbatim}
+
+\newcommand{\grule}{\textrm{\textsl{rule}}}
+\newcommand{\stritem}{\textrm{\textsl{ocaml\_str\_item}}}
+\newcommand{\camlexpr}{\textrm{\textsl{ocaml\_expr}}}
+\newcommand{\arginfo}{\textrm{\textsl{argument\_infos}}}
+\newcommand{\lident}{\textrm{\textsl{lower\_ident}}}
+\newcommand{\argument}{\textrm{\textsl{argument}}}
+\newcommand{\entry}{\textrm{\textsl{entry}}}
+\newcommand{\argtype}{\textrm{\textsl{argtype}}}
+
+\begin{figure}
+\begin{tabular}{|lcll|}
+\hline
+{\stritem}
+ & ::= & 
+\multicolumn{2}{l|}{{\tt TACTIC EXTEND} {\ident} \nelist{\grule}{$|$} {\tt END}}\\
+ & $|$ & \multicolumn{2}{l|}{{\tt VERNAC COMMAND EXTEND} {\ident} \nelist{\grule}{$|$} {\tt END}}\\
+&&\multicolumn{2}{l|}{}\\
+{\grule} & ::= & 
+\multicolumn{2}{l|}{{\tt [} {\str} \sequence{\argument}{} {\tt ] -> [} {\camlexpr} {\tt ]}}\\
+&&\multicolumn{2}{l|}{}\\
+{\argument} & ::= & {\str} &\mbox{(terminal)}\\
+ & $|$ & {\entry} {\tt (} {\lident} {\tt )} &\mbox{(non-terminal)}\\
+&&\multicolumn{2}{l|}{}\\
+{\entry} 
+ & ::= & {\tt string} & (a string)\\
+ & $|$ & {\tt preident} & (an identifier typed as a {\tt string})\\
+ & $|$ & {\tt ident} & (an identifier of type {\tt identifier})\\
+ & $|$ & {\tt global} & (a qualified identifier)\\
+ & $|$ & {\tt constr} & (a {\Coq} term)\\
+ & $|$ & {\tt openconstr} & (a {\Coq} term with holes)\\
+ & $|$ & {\tt sort} & (a {\Coq} sort)\\
+ & $|$ & {\tt tactic} & (an ${\cal L}_{tac}$ expression)\\
+ & $|$ & {\tt constr\_with\_bindings} & (a {\Coq} term with a list of bindings\footnote{as for the tactics {\tt apply} and {\tt elim}})\\
+ & $|$ & {\tt int\_or\_var} & (an integer or an identifier denoting an integer)\\
+ & $|$ & {\tt quantified\_hypothesis} & (a quantified hypothesis\footnote{as for the tactics {\tt intros until}})\\
+ & $|$ & {\tt {\entry}\_opt} & (an optional {\entry} )\\
+ & $|$ & {\tt ne\_{\entry}\_list} & (a non empty list of {\entry})\\
+ & $|$ & {\tt {\entry}\_list} & (a list of {\entry})\\
+ & $|$ & {\tt bool} & (a boolean: no grammar rule, just for typing)\\
+ & $|$ & {\lident} & (a user-defined entry)\\
+\hline
+\end{tabular}
+\caption{Syntax of the macros binding {\ocaml} tactics or commands to a {\Coq} syntax}
+\label{EXTEND-syntax}
+\end{figure}
+
+There is a set of predefined non-terminal entries which are
+automatically translated into an {\ocaml} object of a given type. The
+type is not the same for tactics and for vernacular commands. It is
+given in the following table:
+
+\begin{small}
+\noindent \begin{tabular}{|l|l|l|}
+\hline
+{\entry} & {\it type for tactics} & {\it type for commands} \\
+{\tt string} & {\tt string} & {\tt string}\\
+{\tt preident} & {\tt string} & {\tt string}\\
+{\tt ident} & {\tt identifier} & {\tt identifier}\\
+{\tt global} & {\tt global\_reference} & {\tt qualid}\\
+{\tt constr} & {\tt constr} & {\tt constr\_expr}\\
+{\tt openconstr} & {\tt open\_constr} & {\tt constr\_expr}\\
+{\tt sort} & {\tt sorts} & {\tt rawsort}\\
+{\tt tactic} & {\tt glob\_tactic\_expr * tactic} & {\tt raw\_tactic\_expr}\\
+{\tt constr\_with\_bindings} & {\tt constr with\_bindings} & {\tt constr\_expr with\_bindings}\\\\
+{\tt int\_or\_var} & {\tt int or\_var} & {\tt int or\_var}\\
+{\tt quantified\_hypothesis} & {\tt quantified\_hypothesis} & {\tt quantified\_hypothesis}\\
+{\tt {\entry}\_opt} & {\it the type of entry} {\tt option} & {\it the type of entry} {\tt option}\\
+{\tt ne\_{\entry}\_list} & {\it the type of entry} {\tt list} & {\it the type of entry} {\tt list}\\
+{\tt {\entry}\_list} & {\it the type of entry} {\tt list} & {\it the type of entry} {\tt list}\\
+{\tt bool} & {\tt bool} & {\tt bool}\\
+{\lident} & {user-provided, cf next section} & {user-provided, cf next section}\\
+\hline
+\end{tabular}
+\end{small}
+
+\bigskip
+
+Notice that {\entry} consists in a single identifier and that the {\tt
+\_opt}, {\tt \_list}, ... modifiers are part of the identifier.
+Here is now another example of a tactic which takes either a non empty
+list of identifiers and executes the {\ocaml} function {\tt subst} or
+takes no arguments and executes the{\ocaml} function {\tt subst\_all}.
+
+\begin{verbatim}
+TACTIC EXTEND Subst
+| [ "subst" ne_ident_list(l) ] -> [ subst l ]
+| [ "subst" ] -> [ subst_all ]
+END
+\end{verbatim}
+
+\subsection{Adding grammar entries for tactic or command arguments}
+
+In case parsing the arguments of the tactic or the vernacular command
+involves grammar entries other than the predefined entries listed
+above, you have to declare a new entry using the macros
+\verb=ARGUMENT EXTEND= or \verb=VERNAC ARGUMENT EXTEND=. The syntax is
+given on Figure~\ref{ARGUMENT-EXTEND-syntax}. Notice that arguments
+declared by \verb=ARGUMENT EXTEND= can be used for arguments of both
+tactics and vernacular commands while arguments declared by
+\verb=VERNAC ARGUMENT EXTEND= can only be used by vernacular commands.
+
+For \verb=VERNAC ARGUMENT EXTEND=, the identifier is the name of the
+entry and it must be a valid {\ocaml} identifier (especially it must
+be lowercase).  The grammar rules works as before except that they do
+not have to start by a terminal symbol or word.  As an example, here
+is how the {\Coq} {\tt Extraction Language {\it language}} parses its
+argument:
+
+\begin{verbatim}
+VERNAC ARGUMENT EXTEND language
+| [ "Ocaml" ] -> [ Ocaml ]
+| [ "Haskell" ] -> [ Haskell ]
+| [ "Scheme" ] -> [ Scheme ]
+END
+\end{verbatim}
+
+For tactic arguments, and especially for \verb=ARGUMENT EXTEND=, the
+procedure is more subtle because tactics are objects of the {\Coq}
+environment which can be printed and interpreted. Then the syntax
+requires extra information providing a printer and a type telling how
+the argument behaves. Here is an example of entry parsing a pair of
+optional {\Coq} terms.
+
+\begin{verbatim}
+let pp_minus_div_arg pr_constr pr_tactic (omin,odiv) = 
+  if omin=None && odiv=None then mt() else
+    spc() ++ str "with" ++
+    pr_opt (fun c -> str "minus := " ++ pr_constr c) omin ++
+    pr_opt (fun c -> str "div := " ++ pr_constr c) odiv
+
+ARGUMENT EXTEND minus_div_arg 
+  TYPED AS constr_opt * constr_opt
+  PRINTED BY pp_minus_div_arg
+| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
+| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
+| [ ] -> [ None, None ]
+END
+\end{verbatim}
+
+Notice that the type {\tt constr\_opt * constr\_opt} tells that the
+object behaves as a pair of optional {\Coq} terms, i.e. as an object
+of {\ocaml} type {\tt constr option * constr option} if in a
+\verb=TACTIC EXTEND= macro and of type {\tt constr\_expr option *
+constr\_expr option} if in a \verb=VERNAC COMMAND EXTEND= macro.
+
+As for the printer, it must be a function expecting a printer for
+terms, a printer for tactics and returning a printer for the created
+argument. Especially, each sub-{\term} and each sub-{\tac} in the
+argument must be typed by the corresponding printers. Otherwise, the
+{\ocaml} code will not be well-typed.
+
+\Rem The entry {\tt bool} is bound to no syntax but it can be used to
+give the type of an argument as in the following example:
+
+\begin{verbatim}
+let pr_orient _prc _prt = function
+  | true -> mt ()
+  | false -> str " <-"
+
+ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
+| [ "->" ] -> [ true ]
+| [ "<-" ] -> [ false ]
+| [ ] -> [ true ]
+END
+\end{verbatim}
+
+\begin{figure}
+\begin{tabular}{|lcl|}
+\hline
+{\stritem} & ::= & 
+ {\tt ARGUMENT EXTEND} {\ident} {\arginfo} {\nelist{\grule}{$|$}} {\tt END}\\
+& $|$ & {\tt VERNAC ARGUMENT EXTEND} {\ident} {\nelist{\grule}{$|$}} {\tt END}\\
+\\
+{\arginfo} & ::= & {\tt TYPED AS} {\argtype} \\
+&& {\tt PRINTED BY} {\lident} \\
+%&& \zeroone{{\tt INTERPRETED BY} {\lident}}\\
+%&& \zeroone{{\tt GLOBALIZED BY} {\lident}}\\
+%&& \zeroone{{\tt SUBSTITUTED BY} {\lident}}\\
+%&& \zeroone{{\tt RAW\_TYPED AS} {\lident} {\tt RAW\_PRINTED BY} {\lident}}\\
+%&& \zeroone{{\tt GLOB\_TYPED AS} {\lident} {\tt GLOB\_PRINTED BY} {\lident}}\\
+\\
+{\argtype} & ::= & {\argtype} {\tt *} {\argtype} \\ 
+& $|$ & {\entry} \\
+\hline
+\end{tabular}
+\caption{Syntax of the macros binding {\ocaml} tactics or commands to a {\Coq} syntax}
+\label{ARGUMENT-EXTEND-syntax}
+\end{figure}
+
+%\end{document}