Merge PR #1080: Remove some unused parts of the reference manual.

4 files changed, 1 insertions, 2465 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 0c3b70149..faa9c879c 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -61,7 +61,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
 REFMANTEXFILES:=$(addprefix doc/refman/, \
   headers.sty Reference-Manual.tex \
   RefMan-pre.tex RefMan-int.tex RefMan-com.tex \
-  RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \
+  RefMan-uti.tex RefMan-ide.tex RefMan-modr.tex \
   AsyncProofs.tex RefMan-ssr.tex) \
   $(REFMANCOQTEXFILES) \
 
diff --git a/doc/refman/RefMan-add.tex b/doc/refman/RefMan-add.tex
deleted file mode 100644
index 2094c9d2d..000000000
--- a/doc/refman/RefMan-add.tex
+++ /dev/null
@@ -1,58 +0,0 @@
-\chapter[List of additional documentation]{List of additional documentation\label{Addoc}}
-
-\section[Tutorials]{Tutorials\label{Tutorial}}
-A companion volume to this reference manual, the \Coq\ Tutorial, is
-aimed at gently introducing new users to developing proofs in \Coq\
-without assuming prior knowledge of type theory. In a second step, the
-user can read also the tutorial on recursive types (document {\tt
-RecTutorial.ps}).
-
-\section[The \Coq\ standard library]{The \Coq\ standard library\label{Addoc-library}}
-A brief description of the \Coq\ standard library is given in the additional
-document {\tt Library.dvi}.
-
-\section[Installation and un-installation procedures]{Installation and un-installation procedures\label{Addoc-install}}
-A \verb!INSTALL! file in the distribution explains how to install
-\Coq.
-
-\section[{\tt Extraction} of programs]{{\tt Extraction} of programs\label{Addoc-extract}}
-{\tt Extraction} is a package offering some special facilities to
-extract ML program files. It is described in the separate document
-{\tt Extraction.dvi}
-\index{Extraction of programs}
-
-\section[{\tt Program}]{A tool for {\tt Program}-ing\label{Addoc-program}}
-{\tt Program} is a package offering some special facilities to
-extract ML program files. It is described in the separate document
-{\tt Program.dvi}
-\index{Program-ing}
-
-\section[Proof printing in {\tt Natural} language]{Proof printing in {\tt Natural} language\label{Addoc-natural}}
-{\tt Natural} is a tool to print proofs in natural language.
-It is described in the separate document {\tt Natural.dvi}.
-\index{Natural@{\tt Print Natural}}
-\index{Printing in natural language}
-
-\section[The {\tt Omega} decision tactic]{The {\tt Omega} decision tactic\label{Addoc-omega}}
-{\bf Omega} is a tactic to automatically solve arithmetical goals in
-Presburger arithmetic (i.e. arithmetic without multiplication). 
-It is described in the separate document {\tt Omega.dvi}.
-\index{Omega@{\tt Omega}}
-
-\section[Simplification on rings]{Simplification on rings\label{Addoc-polynom}}
-A documentation of the package {\tt polynom} (simplification on rings)
-can be found in the document {\tt Polynom.dvi}
-\index{Polynom@{\tt Polynom}}
-\index{Simplification on rings}
-
-%\section[Anomalies]{Anomalies\label{Addoc-anomalies}}
-%The separate document {\tt Anomalies.*} gives a list of known
-%anomalies and bugs of the system.  Before communicating us an
-%anomalous behavior, please check first whether it has been already
-%reported in this document.
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex
deleted file mode 100644
index dac3c60bd..000000000
--- a/doc/refman/RefMan-coi.tex
+++ /dev/null
@@ -1,405 +0,0 @@
-%\documentstyle[11pt,../tools/coq-tex/coq]{article}
-%\input{title}
- 
-%\include{macros}
-%\begin{document}
-
-%\coverpage{Co-inductive types in Coq}{Eduardo Gim\'enez}
-\chapter[Co-inductive types in Coq]{Co-inductive types in Coq\label{Co-inductives}}
-
-%\begin{abstract}
-{\it Co-inductive} types are types whose elements may not be well-founded.
-A formal study of the Calculus of Constructions extended by 
-co-inductive types has been presented
-in \cite{Gim94}. It is based on the notion of
-{\it guarded definitions} introduced by Th. Coquand
-in \cite{Coquand93}. The implementation is by E. Gim\'enez.
-%\end{abstract}
-
-\section{A short introduction to co-inductive types}
-
-We assume that the reader is rather familiar with inductive types.
-These types are characterized by their {\it constructors}, which can be 
-regarded as the basic methods from which the elements 
-of the type can be built up. It is implicit in the definition 
-of an inductive type that 
-its elements are the result of a {\it finite} number of 
-applications of its constructors. Co-inductive types arise from 
-relaxing this implicit condition and admitting that an element of
-the type can also be introduced by a non-ending (but effective) process 
-of construction defined in terms of the basic methods which characterize the
-type. So we could think in the wider notion of types defined by
-constructors (let us call them {\it recursive types}) and classify
-them into inductive and co-inductive ones, depending on whether or not
-we consider non-ending methods as admissible for constructing elements
-of the type. Note that in both cases we obtain a ``closed type'', all whose 
-elements are pre-determined in advance (by the constructors). When we
-know that $a$ is an element of a recursive type (no matter if it is 
-inductive or co-inductive) what we know is that it is the result of applying
-one of the basic forms of construction allowed for the type.
-So the more primitive way of eliminating an element of a recursive type is 
-by case analysis, i.e. by considering through which constructor it could have
-been introduced. In the case of inductive sets, the additional knowledge that
-constructors can be applied only a finite number of times provide
-us with a more powerful way of eliminating their elements, say,  
-the principle of
-induction. This principle is obviously not valid for co-inductive types,
-since it is just the expression of this extra knowledge attached to inductive 
-types.
-
-
-An example of a co-inductive type is the type of infinite sequences formed with
-elements of type $A$, or streams for shorter. In Coq, 
-it can be introduced using the \verb!CoInductive! command~:
-\begin{coq_example}
-CoInductive Stream (A:Set) : Set :=
-    cons : A -> Stream A -> Stream A.
-\end{coq_example}
-
-The syntax of this command is the same as the 
-command \verb!Inductive! (cf. section
-\ref{gal_Inductive_Definitions}).
-Definition of mutually co-inductive types are possible.
-
-As was already said, there are not principles of 
-induction for co-inductive sets, the only way of eliminating these
-elements is by case analysis. 
-In the example of streams, this elimination principle can be
-used for instance to define the well known 
-destructors on streams $\hd : (\Str\;A)\rightarrow A$ 
-and $\tl: (\Str\;A)\rightarrow (\Str\;A)$  :
-\begin{coq_example}
-Section Destructors.
-Variable A : Set.
-Definition hd (x:Stream A) := match x with
-                              | cons a s => a
-                              end.
-Definition tl (x:Stream A) := match x with
-                              | cons a s => s
-                              end.
-\end{coq_example}
-\begin{coq_example*}
-End Destructors.
-\end{coq_example*}
-
-\subsection{Non-ending methods of construction}
-
-At this point the reader should have realized that we have left unexplained
-what is a ``non-ending but effective process of
-construction'' of a stream. In the widest sense, a 
-method is a non-ending process of construction if we can eliminate the
-stream that it introduces, in other words, if we can reduce
-any case analysis on it. In this sense, the following ways of 
-introducing a stream are not acceptable. 
-\begin{center}
-$\zeros = (\cons\;\nat\;\nO\;(\tl\;\zeros))\;\;:\;\;(\Str\;\nat)$\\[12pt]
-$\filter\;(\cons\;A\;a\;s) = \si\;\;(P\;a)\;\;\alors\;\;(\cons\;A\;a\;(\filter\;s))\;\;\sinon\;\;(\filter\;s) )\;\;:\;\;(\Str\;A)$
-\end{center}
-\noindent The former it is not valid since the stream can not be eliminated 
-to obtain its tail. In the latter, a stream is naively defined as
-the result of erasing from another (arbitrary) stream 
-all the elements which does not verify a certain property $P$. This
-does not always makes sense, for example it does not when all the elements
-of the stream verify $P$, in which case we can not eliminate it to
-obtain its head\footnote{Note that there is no notion of ``the empty
-stream'', a stream is always infinite and build by a \texttt{cons}.}. 
-On the contrary, the following definitions are acceptable methods for
-constructing a stream~:
-\begin{center}
-$\zeros = (\cons\;\nat\;\nO\;\zeros)\;\;:\;\;(\Str\;\nat)\;\;\;(*)$\\[12pt]
-$(\from\;n) = (\cons\;\nat\;n\;(\from\;(\nS\;n)))\;:\;(\Str\;\nat)$\\[12pt]
-$\alter  = (\cons\;\bool\;\true\;(\cons\;\bool\;\false\;\alter))\;:\;(\Str\;\bool)$.
-\end{center}
-\noindent The first one introduces a stream containing all the natural numbers
-greater than a given one, and the second the stream which infinitely
-alternates the booleans true and false.
-
-In general it is not evident to realise when a definition can 
-be accepted or not. However, there is a class of definitions that
-can be easily recognised as being valid :  those 
-where (1) all the recursive calls of the method  are done 
-after having explicitly mentioned  which is (at least) the first constructor 
-to start building the element, and (2) no other 
-functions apart from constructors are applied to recursive calls. 
-This class of definitions is usually
-referred as {\it guarded-by-constructors} 
-definitions \cite{Coquand93,Gim94}. 
-The methods $\from$ 
-and $\alter$ are examples of definitions which are guarded by constructors.
-The definition of function $\filter$ is not, because there is no 
-constructor to guard 
-the recursive call in the {\it else} branch. Neither is the one of
-$\zeros$, since there is function applied to the recursive call
-which is not a constructor. However, there is a difference between 
-the definition of $\zeros$ and $\filter$. The former may be seen as a
-wrong way of characterising an object which makes sense, and it can
-be reformulated in an admissible way using the equation (*). On the contrary, 
-the definition of
-$\filter$ can not be patched, since is the idea itself 
-of traversing an infinite
-construction searching for an element whose existence is not ensured
-which does not make sense.
-
-
-
-Guarded definitions are exactly the kind of non-ending process of 
-construction which are allowed in Coq. The way of introducing 
-a guarded definition in Coq is using the special command 
-{\tt CoFixpoint}.  This command verifies that the definition introduces an
-element of a co-inductive type, and checks if it is guarded by constructors. 
-If we try to 
-introduce the definitions above, $\from$ and $\alter$ will be accepted,
-while $\zeros$ and $\filter$ will be rejected giving some explanation 
-about why.
-\begin{coq_example}
-CoFixpoint zeros  : Stream nat := cons nat 0%N (tl nat zeros).
-CoFixpoint zeros  : Stream nat := cons nat 0%N zeros.
-CoFixpoint from (n:nat) : Stream nat := cons nat n (from (S n)).
-\end{coq_example}
-
-As in the \verb!Fixpoint! command (see Section~\ref{Fixpoint}), it is possible 
-to introduce a block of mutually dependent methods. The general syntax
-for this case is :
-
-{\tt CoFixpoint {\ident$_1$}  :{\term$_1$} := {\term$_1'$}\\
-     with\\
-        \mbox{}\hspace{0.1cm} $\ldots$  \\
-        with {\ident$_m$}   : {\term$_m$} := {\term$_m'$}}
-
-
-\subsection{Non-ending methods and reduction}
-
-The elimination of a stream introduced by a \verb!CoFixpoint! definition 
-is done lazily, i.e. its definition can be expanded only when it occurs 
-at the head of an application which is the argument of a case expression. 
-Isolately it is considered as a canonical expression which 
-is completely evaluated. We can test this using the command \verb!compute! 
-to calculate the normal forms of some terms~:
-\begin{coq_example}
-Eval compute in (from 0).
-Eval compute in (hd nat (from 0)).
-Eval compute in (tl nat (from 0)).
-\end{coq_example}
-\noindent Thus, the equality 
-$(\from\;n)\equiv(\cons\;\nat\;n\;(\from \; (\S\;n)))$
-does not hold as definitional one. Nevertheless, it can be proved 
-as a propositional  equality, in the sense of Leibniz's equality. 
-The version {\it à la Leibniz} of the equality above follows from
-a general lemma stating that eliminating and then re-introducing a stream
-yields the same stream.
-\begin{coq_example}
-Lemma unfold_Stream :
-   forall x:Stream nat, x = match x with
-                            | cons a s => cons nat a s
-                            end.
-\end{coq_example}
- 
-\noindent The proof is immediate from the analysis of 
-the possible cases for $x$, which transforms 
-the equality in a trivial one.
-
-\begin{coq_example}
-olddestruct x.
-trivial.
-\end{coq_example}
-\begin{coq_eval}
-Qed.
-\end{coq_eval}
-The application of this lemma to  $(\from\;n)$ puts this
-constant at the head of an application which is an  argument 
-of a case analysis, forcing its expansion. 
-We can test the type of this application using Coq's command \verb!Check!,
-which infers the type of a given term. 
-\begin{coq_example}
-Check (fun n:nat => unfold_Stream (from n)).
-\end{coq_example}
- \noindent  Actually, The elimination of $(\from\;n)$ has actually 
-no effect, because it is followed by a re-introduction, 
-so the type of this application is in fact 
-definitionally equal to the
-desired proposition. We can test this computing
-the normal form of the application above to see its type.  
-\begin{coq_example}
-Transparent unfold_Stream.
-Eval compute in (fun n:nat => unfold_Stream (from n)).
-\end{coq_example}
-
-
-\section{Reasoning about infinite objects}
-
-At a first sight, it might seem that 
-case analysis does not provide a very powerful way
-of reasoning about infinite objects. In fact, what we can prove about 
-an infinite object using
-only case analysis is just what we can prove unfolding its method
-of construction a finite number of times, which is not always
-enough. Consider for example the following method for appending 
-two streams~:
-\begin{coq_example}
-Variable A : Set.
-CoFixpoint conc (s1 s2:Stream A) : Stream A :=
-  cons A (hd A s1) (conc (tl A s1) s2).
-\end{coq_example}
-
-Informally speaking, we expect that for all pair of streams $s_1$ and $s_2$, 
-$(\conc\;s_1\;s_2)$ 
-defines the ``the same'' stream as $s_1$, 
-in the sense that if we would be able to unfold the definition 
-``up to the infinite'', we would obtain definitionally equal normal forms.
-However, no finite unfolding of the definitions gives definitionally 
-equal terms. Their equality can not be proved just using case analysis.
-
-
-The weakness of the elimination principle proposed for infinite objects
-contrast with the power provided by the inductive 
-elimination principles, but it is not actually surprising. It just means
-that we can not expect to prove very interesting things about infinite
-objects doing finite proofs. To take advantage of infinite objects we
-have to consider infinite proofs as well. For example,
-if we want to catch up the equality between $(\conc\;s_1\;s_2)$ and 
-$s_1$ we have to introduce first the type of the infinite proofs 
-of equality between streams. This is a 
-co-inductive type, whose elements are build up from a 
-unique constructor, requiring a proof of the equality of the
-heads of the streams, and an (infinite) proof of the equality 
-of their tails. 
-
-\begin{coq_example}
-CoInductive EqSt : Stream A -> Stream A -> Prop :=
-    eqst :
-      forall s1 s2:Stream A,
-        hd A s1 = hd A s2 -> EqSt (tl A s1) (tl A s2) -> EqSt s1 s2.
-\end{coq_example}
-\noindent Now the equality of both streams can be proved introducing
-an infinite object of type 
-
-\noindent $(\EqSt\;s_1\;(\conc\;s_1\;s_2))$ by a \verb!CoFixpoint!
-definition.
-\begin{coq_example}
-CoFixpoint eqproof (s1 s2:Stream A) : EqSt s1 (conc s1 s2) :=
-  eqst s1 (conc s1 s2) (eq_refl (hd A (conc s1 s2)))
-    (eqproof (tl A s1) s2).
-\end{coq_example}
-\begin{coq_eval}
-Reset eqproof.
-\end{coq_eval}
-\noindent Instead of giving an explicit definition, 
-we can use the proof editor of Coq to help us in 
-the construction of the proof.
-A tactic \verb!Cofix! allows placing a \verb!CoFixpoint! definition
-inside a proof. 
-This tactic introduces a variable in the context which has
-the same type as the current goal, and its application stands
-for a recursive call in the construction of the proof. If no name is
-specified for this variable, the name of the lemma  is chosen by
-default.
-%\pagebreak 
-
-\begin{coq_example}
-Lemma eqproof : forall s1 s2:Stream A, EqSt s1 (conc s1 s2).
-cofix.
-\end{coq_example}
-
-\noindent An easy (and wrong!) way of finishing the proof is just to apply the
-variable \verb!eqproof!, which has the same type as the goal. 
-
-\begin{coq_example}
-intros.
-apply eqproof.
-\end{coq_example}
-
-\noindent The ``proof'' constructed in this way 
-would correspond to the \verb!CoFixpoint! definition
-\begin{coq_example*}
-CoFixpoint eqproof  : forall s1 s2:Stream A, EqSt s1 (conc s1 s2) :=
-  eqproof.
-\end{coq_example*}
-
-\noindent which is obviously non-guarded. This means that 
-we can use the proof editor to
-define a method of construction which does not make sense. However,
-the system will never accept to include it as part of the theory,
-because the guard condition is always verified before saving the proof.
-
-\begin{coq_example}
-Qed.
-\end{coq_example}
-
-\noindent Thus, the user must be careful in the 
-construction of infinite proofs 
-with the tactic \verb!Cofix!. Remark that once it has been used 
-the application of tactics performing automatic proof search in 
-the environment (like for example \verb!Auto!)
-could introduce unguarded recursive calls in the proof.
-The command \verb!Guarded! verifies
-that the guarded condition has been not violated 
-during the construction of the proof. This command can be
-applied even if the proof term is not complete.
-
-
-
-\begin{coq_example}
-Restart.
-cofix.
-auto.
-Guarded.
-Undo.
-Guarded.
-\end{coq_example}
-
-\noindent To finish with this example, let us restart from the
-beginning and show how to construct an admissible proof~:
-
-\begin{coq_example} 
-Restart.
- cofix.
-\end{coq_example}
-
-%\pagebreak
-
-\begin{coq_example}
-intros.
-apply eqst.
-trivial.
-simpl.
-apply eqproof.
-Qed.
-\end{coq_example}
-
-
-\section{Experiments with co-inductive types}
-
-Some examples involving co-inductive types are available with
-the distributed system, in the theories library and in the contributions
-of the Lyon site. Here we present a short description of their contents~:
-\begin{itemize}
-\item Directory \verb!theories/LISTS! : 
-        \begin{itemize}
-                \item File \verb!Streams.v! : The type of streams and the 
-extensional equality between streams. 
-        \end{itemize}
-
-\item Directory \verb!contrib/Lyon/COINDUCTIVES! : 
-      \begin{itemize}
-                \item Directory \verb!ARITH! : An arithmetic where $\infty$
-is an explicit constant of the language instead of a metatheoretical notion.
-                \item Directory \verb!STREAM! :
-      \begin{itemize}
-                \item File \verb!Examples! :
-Several examples of guarded definitions, as well as 
-of frequent errors in the introduction of a stream. A different 
-way of defining the extensional equality of two streams,
-and the proofs showing that it is equivalent to the one in \verb!theories!.
-                \item File \verb!Alter.v! : An example showing how 
-an infinite proof introduced by a guarded definition can be also described
-using an operator of co-recursion \cite{Gimenez95b}.
-                 \end{itemize}
-\item Directory \verb!PROCESSES! : A proof of the alternating 
-bit protocol based on Pra\-sad's Calculus of Broadcasting Systems \cite{Prasad93},
-and the verification of an interpreter for this calculus. 
-See \cite{Gimenez95b} for a complete description about this development.
-        \end{itemize}
-\end{itemize}
-
-%\end{document}
-
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
deleted file mode 100644
index 7e5bb81a9..000000000
--- a/doc/refman/RefMan-tus.tex
+++ /dev/null
@@ -1,2001 +0,0 @@
-%\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 de Bruijn's binder on the term $t$;
-\item $\texttt{DLAMV}\;(x,vt)$, a de Bruijn'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 de Bruijn'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 de Bruijn'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 de Bruijn'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 de Bruijn'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 
-     de Bruijn'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 de Bruijn'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 de Bruijn'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} 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.user_err : ?loc:Loc.t -> 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}