1 files changed, 0 insertions, 393 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
deleted file mode 100644
index 208a014a..00000000
--- a/doc/refman/RefMan-pro.tex
+++ /dev/null
@@ -1,393 +0,0 @@
-\chapter{Proof handling}
-\index{Proof editing}
-\label{Proof-handling}
-
-In \Coq's proof editing mode all top-level commands documented in 
-chapter \ref{Vernacular-commands} remain available
-and the user has access to specialized commands dealing with proof
-development pragmas documented in this section. He can also use some
-other specialized commands called {\em tactics}.  They are the very
-tools allowing the user to deal with logical reasoning. They are
-documented in chapter \ref{Tactics}.\\ 
-When switching in editing proof mode, the prompt
-\index{Prompt} 
-{\tt Coq <} is changed into {\tt {\ident} <} where {\ident} is the
-declared name of the theorem currently edited.
-
-At each stage of a proof development, one has a list of goals to
-prove. Initially, the list consists only in the theorem itself. After
-having applied some tactics, the list of goals contains the subgoals
-generated by the tactics.
-
-To each subgoal is associated  a number of
-hypotheses we call the {\em \index*{local context}} of the goal.
-Initially, the local context is empty. It is enriched by the use of
-certain tactics (see mainly section~\ref{intro}).
-
-When a proof is achieved the message {\tt Proof completed} is
-displayed. One can then store this proof as a defined constant in the
-environment. Because there exists a correspondence between proofs and
-terms of $\lambda$-calculus, known as the {\em Curry-Howard
-isomorphism} \cite{How80,Bar91,Gir89,Hue89}, \Coq~ stores proofs as
-terms of {\sc Cic}. Those terms are called {\em proof
-  terms}\index{Proof term}.
-
-It is possible to edit several proofs at the same time: see section
-\ref{Resume}
-
-\ErrMsg When one attempts to use a proof editing command out of the
-proof editing mode, \Coq~ raises the error message : \errindex{No focused
-  proof}.
-
-\section{Switching on/off the proof editing mode}
-
-\subsection{\tt Goal {\form}.}
-\comindex{Goal}\label{Goal}
-This command switches \Coq~ to editing proof mode and sets {\form} as
-the original goal. It associates the name {\tt Unnamed\_thm} to
-that goal.
-
-\begin{ErrMsgs}
-\item \errindex{the term \form\ has type \ldots{} which should be Set,
-    Prop or Type}
-%\item \errindex{Proof objects can only be abstracted}
-%\item \errindex{A goal should be a type}
-%\item \errindex{repeated goal not permitted in refining mode}
-%the command {\tt Goal} cannot be used while a proof is already being edited.
-\end{ErrMsgs}
-
-\SeeAlso section \ref{Theorem}
-
-\subsection{\tt Qed.}\comindex{Qed}\label{Qed}
-This command is available in interactive editing proof mode when the
-proof is completed.  Then {\tt Qed} extracts a proof term from the
-proof script, switches back to {\Coq} top-level and attaches the
-extracted proof term to the declared name of the original goal. This
-name is added to the environment as an {\tt Opaque} constant.
-
-\begin{ErrMsgs}
-\item \errindex{Attempt to save an incomplete proof}
-%\item \ident\ \errindex{already exists}\\ 
-%  The implicit name is already defined. You have then to provide
-%  explicitly a new name (see variant 3 below).
-\item Sometimes an error occurs when building the proof term,
-because tactics do not enforce completely the term construction
-constraints.
-
-The user should also be aware of the fact that since the proof term is
-completely rechecked at this point, one may have to wait a while when
-the proof is large. In some exceptional cases one may even incur a
-memory overflow.
-\end{ErrMsgs}
-
-\begin{Variants}
-
-\item {\tt Defined.}
-\comindex{Defined} 
-\label{Defined} 
-
-  Defines the proved term as a transparent constant.
-
-\item {\tt Save.}
-\comindex{Save}
-
-  Is equivalent to {\tt Qed}.
-
-\item {\tt Save {\ident}.}
-  
-  Forces the name of the original goal to be {\ident}.  This command
-  (and the following ones) can only be used if the original goal has
-  been opened using the {\tt Goal} command.
-
-\item {\tt Save Theorem {\ident}.} \\
- {\tt Save Lemma {\ident}.} \\
- {\tt Save Remark {\ident}.}\\
- {\tt Save Fact {\ident}.}
-
-  Are equivalent to {\tt Save {\ident}.} 
-\end{Variants}
-
-\subsection{\tt Admitted.}\comindex{Admitted}\label{Admitted}
-This command is available in interactive editing proof mode to give up
-the current proof and declare the initial goal as an axiom.
-
-\subsection{\tt Theorem {\ident} : {\form}.}
-\comindex{Theorem}
-\label{Theorem}
-
-This command switches to interactive editing proof mode and declares
-{\ident} as being the name of the original goal {\form}. When declared
-as a {\tt Theorem}, the name {\ident} is known at all section levels:
-{\tt Theorem} is a {\sl global} lemma.
-
-%\ErrMsg (see section \ref{Goal})
-
-\begin{ErrMsgs}
-
-\item \errindex{the term \form\ has type \ldots{} which should be Set,
-    Prop or Type}
-
-\item \errindexbis{\ident already exists}{already exists}
- 
-  The name you provided already defined. You have then to choose
-  another name.
-
-\end{ErrMsgs}
-
-
-\begin{Variants}
-
-\item {\tt Lemma {\ident} : {\form}.}
-\comindex{Lemma}
-
-  It is equivalent to {\tt Theorem {\ident} : {\form}.}
-
-\item {\tt Remark {\ident} : {\form}.}\comindex{Remark}\\
-  {\tt Fact {\ident} : {\form}.}\comindex{Fact}
-
-  Used to have a different meaning, but are now equivalent to {\tt
-  Theorem {\ident} : {\form}.} They are kept for compatibility.
-
-\item {\tt Definition {\ident} : {\form}.}
-\comindex{Definition}
-
-  Analogous to {\tt Theorem}, intended to be used in conjunction with
-  {\tt Defined} (see \ref{Defined}) in order to define a
-  transparent constant.
-
-\item {\tt Let {\ident} : {\form}.}
-\comindex{Let}
-
-  Analogous to {\tt Definition} except that the definition is turned
-  into a local definition on objects depending on it after closing the
-  current section.
-\end{Variants}
-
-\subsection{\tt Proof {\term}.}
-\comindex{Proof}
-\label{BeginProof}
-This command applies in proof editing mode. It is equivalent to {\tt
-  exact {\term}; Save.} That is, you have to give the full proof in
-one gulp, as a proof term (see section \ref{exact}).
-
-\variant {\tt Proof.}
-  
-  Is a noop which is useful to delimit the sequence of tactic commands
-  which start a proof, after a {\tt Theorem} command.  It is a good
-  practice to use {\tt Proof.} as an opening parenthesis, closed in
-  the script with a closing {\tt Qed.}
-
-\SeeAlso {\tt Proof with {\tac}.} in section~\ref{ProofWith}.
-
-\subsection{\tt Abort.}
-\comindex{Abort}
-
-This command cancels the current proof development, switching back to
-the previous proof development, or to the \Coq\ toplevel if no other
-proof was edited.
-
-\begin{ErrMsgs}
-\item \errindex{No focused proof (No proof-editing in progress)}
-\end{ErrMsgs}
-
-\begin{Variants}
-
-\item {\tt Abort {\ident}.}
-
-  Aborts the editing of the proof named {\ident}.
-
-\item {\tt Abort All.}
-
-  Aborts all current goals, switching back to the \Coq\ toplevel.
-
-\end{Variants}
-
-\subsection{\tt Suspend.}
-\comindex{Suspend}
-
-This command applies in proof editing mode. It switches back to the
-\Coq\ toplevel, but without canceling the current proofs.
-
-\subsection{\tt Resume.}
-\comindex{Resume}\label{Resume}
-
-This commands switches back to the editing of the last edited proof.
-
-\begin{ErrMsgs}
-\item \errindex{No proof-editing in progress}
-\end{ErrMsgs}
-
-\begin{Variants}
-
-\item {\tt Resume {\ident}.}
-
-  Restarts the editing of the proof named {\ident}. This can be used
-  to navigate between currently edited proofs.
-
-\end{Variants}
-
-\begin{ErrMsgs}
-\item \errindex{No such proof}
-\end{ErrMsgs}
-
-\section{Navigation in the proof tree}
-
-\subsection{\tt Undo.}
-\comindex{Undo}
-
-This command cancels the effect of the last tactic command.  Thus, it
-backtracks one step.
-
-\begin{ErrMsgs}
-\item \errindex{No focused proof (No proof-editing in progress)}
-\item \errindex{Undo stack would be exhausted}
-\end{ErrMsgs}
-
-\begin{Variants}
-
-\item {\tt Undo {\num}.}
-
-  Repeats {\tt Undo} {\num} times.
-
-\end{Variants}
-
-\subsection{\tt Set Undo {\num}.}
-\comindex{Set Undo}
-
-This command changes the maximum number of {\tt Undo}'s that will be
-possible when doing a proof. It only affects proofs started after
-this command, such that if you want to change the current undo limit
-inside a proof, you should first restart this proof.
-
-\subsection{\tt Unset Undo.}
-\comindex{Unset Undo}
-
-This command resets the default number of possible {\tt Undo} commands
-(which is currently 12).
-
-\subsection{\tt Restart.}\comindex{Restart}
-This command restores the proof editing process to the original goal.
-
-\begin{ErrMsgs}
-\item \errindex{No focused proof to restart}
-\end{ErrMsgs}
-
-\subsection{\tt Focus.}\comindex{Focus}
-This focuses the attention on the first subgoal to prove and the printing
-of the other subgoals is suspended until the focused subgoal is
-solved or unfocused. This is useful when there are many current
-subgoals which clutter your screen.
-
-\begin{Variant}
-\item {\tt Focus {\num}.}\\ 
-This focuses the attention on the $\num^{\scriptsize th}$ subgoal to prove.
-
-\end{Variant}
-
-\subsection{\tt Unfocus.}\comindex{Unfocus}
-Turns off the focus mode.
-
-
-\section{Displaying information}
-
-\subsection{\tt Show.}\comindex{Show}\label{Show}
-This command displays the current goals.
-
-\begin{Variants}
-\item {\tt Show {\num}.}\\ 
-  Displays only the {\num}-th subgoal.\\ 
-\begin{ErrMsgs}
-\item \errindex{No such goal}
-\item \errindex{No focused proof}
-\end{ErrMsgs}
-
-\item {\tt Show Implicits.}\comindex{Show Implicits}\\
-  Displays the current goals, printing the implicit arguments of
-  constants.
-
-\item {\tt Show Implicits {\num}.}\\
-  Same as above, only displaying the {\num}-th subgoal.
-
-\item {\tt Show Script.}\comindex{Show Script}\\
-  Displays the whole list of tactics applied from the beginning
-  of the current proof. 
-  This tactics script may contain some holes (subgoals not yet proved).
-  They are printed under the form \verb!<Your Tactic Text here>!.
-
-\item {\tt Show Tree.}\comindex{Show Tree}\\
-This command can be seen as a more structured way of
-displaying the state of the proof than that 
-provided by {\tt Show Script}. Instead of just giving
-the list of tactics that have been applied, it 
-shows the derivation tree constructed by then. 
-Each node of the tree contains the conclusion
-of the corresponding sub-derivation (i.e. a
-goal with its corresponding local context) and 
-the tactic that has generated all the 
-sub-derivations. The leaves of this tree are
-the goals which still remain to be proved.
-
-%\item {\tt Show Node}\comindex{Show Node}\\
-%        Not yet documented
-
-\item {\tt Show Proof.}\comindex{Show Proof}\\
-It displays the proof term generated by the 
-tactics that have been applied. 
-If the proof is not completed, this term contain holes,
-which correspond to the sub-terms which are still to be 
-constructed. These holes appear as a question mark indexed 
-by an integer, and applied to the list of variables in 
-the context, since it may depend on them. 
-The types obtained by abstracting away the context from the
-type of each hole-placer are also printed.
-
-\item {\tt Show Conjectures.}\comindex{Show Conjectures}\\
-It prints the list of the names of all the theorems that 
-are currently being proved.
-As it is possible to start proving a previous lemma during
-the proof of a theorem, this list may contain several 
-names. 
-
-\item{\tt Show Intro.}\comindex{Show Intro}\\
-If the current goal begins by at least one product, this command
-prints the name of the first product, as it would be generated by 
-an anonymous {\tt Intro}. The aim of this command is to ease the
-writing of more robust scripts. For example, with an appropriate 
-Proof General macro, it is possible to transform any anonymous {\tt
-  Intro} into a qualified one such as {\tt Intro y13}.
-In the case of a non-product goal, it prints nothing. 
-
-\item{\tt Show Intros.}\comindex{Show Intros}\\
-This command is similar to the previous one, it simulates the naming 
-process of an {\tt Intros}.
-
-\end{Variants}
-
-\subsection{\tt Set Hyps Limit {\num}.}
-\comindex{Set Hyps Limit}
-This command sets the maximum number of hypotheses displayed in
-goals after the application of a tactic. 
-All the hypotheses remains usable in the proof development.
-
-\subsection{\tt Unset Hyps Limit.}
-\comindex{Unset Hyps Limit}
-This command goes back to the default mode which is to print all
-available hypotheses.
-
-\section{$DPL$ : A Declarative proof language for Coq \emph{(experimental)} }
-
-An implementation of the $DPL$ declarative proof language by Pierre Corbineau at the Radboud University Nijmegen (The Netherlands) is included in Coq.
-
- Due to the experimental nature and hence the potentially unstable semantics of the language, its documentation is not included here. However, it can be found at :
-
-\url{http://www.cs.ru.nl/~corbineau/mmode.html}
-
-
-
-
-% $Id: RefMan-pro.tex 9286 2006-10-26 17:43:00Z corbinea $
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: