Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".

Updated documentation in many ways:
- merged binder and binderlet as done for a while in implementation
- fixed a few technical problems (bad indexation of {x:A|P x}, missing
  spaces in html code in many situations due to missing curly brackets
  around TeX macros - e.g. around \ldots -, missing dots at end of
  sentences, ...)
- renamed "statement" commands into "assertion" commands and
  "declaration" commands into "assumption" commands
- moved Goal and Save out of the Gallina chapter
- avoid some recovering in the Gallina and proof mode chapters
- slight smoothing of some hard-to-read paragraphs of the manual

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13091 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 49 insertions, 74 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index a8bb7966a..d73ab5d2c 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -19,20 +19,23 @@ 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
+hypotheses called the {\em \index*{local context}} of the goal.
+Initially, the local context contains the local variables and
+hypotheses of the current section (see Section~\ref{Variable}) and the
+local variables and hypotheses of the theorem statement.  It is
+enriched by the use of certain tactics (see e.g. {\tt intro} in
+Section~\ref{intro}).
+
+When a proof is completed, the message {\tt Proof completed} is
+displayed. One can then register 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}
+It is possible to edit several proofs in parallel: 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
@@ -40,21 +43,25 @@ proof editing mode, \Coq~ raises the error message : \errindex{No focused
 
 \section{Switching on/off the proof editing mode}
 
-\subsection[\tt Goal {\form}.]{\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.
+The proof editing mode is entered by asserting a statement, which
+typically is the assertion of a theorem:
 
-\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}
+\begin{quote}
+{\tt Theorem {\ident} \zeroone{\binders} : {\form}.\comindex{Theorem}
+\label{Theorem}}
+\end{quote}
+
+The list of assertion commands is given in
+Section~\ref{Assertions}. The command {\tt Goal} can also be used.
 
-\SeeAlso Section~\ref{Theorem}
+\subsection[Goal {\form}.]{\tt Goal {\form}.\comindex{Goal}\label{Goal}}
+
+This is intended for quick assertion of statements, without knowing in
+advance which name to give to the assertion, typically for quick
+testing of the provability of a statement. If the proof of the
+statement is eventually completed and validated, the statement is then
+bound to the name {\tt Unnamed\_thm} (or a variant of this name not
+already used for another statement).
 
 \subsection[\tt Qed.]{\tt Qed.\comindex{Qed}\label{Qed}}
 This command is available in interactive editing proof mode when the
@@ -89,7 +96,7 @@ memory overflow.
 \item {\tt Save.}
 \comindex{Save}
 
-  Is equivalent to {\tt Qed}.
+  This is a deprecated equivalent to {\tt Qed}.
 
 \item {\tt Save {\ident}.}
   
@@ -101,6 +108,8 @@ memory overflow.
  {\tt Save Lemma {\ident}.} \\
  {\tt Save Remark {\ident}.}\\
  {\tt Save Fact {\ident}.}
+ {\tt Save Corollary {\ident}.}
+ {\tt Save Proposition {\ident}.}
 
   Are equivalent to {\tt Save {\ident}.} 
 \end{Variants}
@@ -109,57 +118,6 @@ memory overflow.
 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}.]{\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}.]{\tt Proof {\term}.\comindex{Proof}
 \label{BeginProof}}
 This command applies in proof editing mode. It is equivalent to {\tt
@@ -234,7 +192,7 @@ This command allows to instantiate an existential variable. {\tt \num}
 is an index in the list of uninstantiated existential variables
 displayed by {\tt Show Existentials.} (described in Section~\ref{Show})
 
-This command is intented to be used to instantiate existential
+This command is intended to be used to instantiate existential
 variables when the proof is completed but some uninstantiated
 existential variables remain. To instantiate existential variables
 during proof edition, you should use the tactic {\tt instantiate}.
@@ -392,6 +350,8 @@ fixpoint and cofixpoint is violated at some time of the construction
 of the proof without having to wait the completion of the proof."
 
 
+\section{Controlling the effect of proof editing commands}
+
 \subsection[\tt Set Hyps Limit {\num}.]{\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. 
@@ -402,6 +362,21 @@ All the hypotheses remains usable in the proof development.
 This command goes back to the default mode which is to print all
 available hypotheses.
 
+
+\subsection[\tt Set Automatic Introduction.]{\tt Set Automatic Introduction.\comindex{Set Automatic Introduction}\comindex{Unset Automatic Introduction}\label{Set Automatic Introduction}}
+
+The option {\tt Automatic Introduction} controls the way binders are
+handled in assertion commands such as {\tt Theorem {\ident}
+  \zeroone{\binders} : {\form}}. When the option is set, which is the
+default, {\binders} are automatically put in the local context of the
+goal to prove.
+
+The option can be unset by issuing {\tt Unset Automatic Introduction}.
+When the option is unset, {\binders} are discharged on the statement
+to be proved and a tactic such as {\tt intro} (see
+Section~\ref{intro}) has to be used to move the assumptions to the
+local context.
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"