Erreurs de derniere minute

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

2 files changed, 56 insertions, 81 deletions

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index ea86c3994..0b9f7b7b5 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -2184,59 +2184,59 @@ Proof-search is bounded by a depth parameter which can be set by typing the
 {\nobreak \tt Set Firstorder Depth $n$} \comindex{Set Firstorder Depth} 
 vernacular command.
 
-\subsection{{\tt jp} {\em (Jprover)}
-\tacindex{jp}
-\label{jprover}}
-
-The tactic \texttt{jp}, due to Huang Guan-Shieng, is an experimental
-port of the {\em Jprover}\cite{SLKN01} semi-decision procedure for
-first-order intuitionistic logic implemented in {\em
-  NuPRL}\cite{Kre02}.
-
-The tactic \texttt{jp}, due to Huang Guan-Shieng, is an {\it
-  experimental} port of the {\em Jprover}\cite{SLKN01} semi-decision 
-procedure for first-order intuitionistic logic implemented in {\em
-  NuPRL}\cite{Kre02}. 
-
-Search may optionnaly be bounded by a multiplicity parameter
-indicating how many (at most) copies of a formula may be used in 
-the proof process, its absence may lead to non-termination of the tactic.
-
-%\begin{coq_eval}
-%Variable S:Set.
-%Variables P Q:S->Prop.
-%Variable f:S->S.
-%\end{coq_eval}
-
-%\begin{coq_example*}
-%Lemma example: (exists x |P x\/Q x)->(exists x |P x)\/(exists x |Q x).
-%jp.
-%Qed.
-
-%Lemma example2: (forall x ,P x->P (f x))->forall x,P x->P (f(f x)).
-%jp.
-%Qed.
-%\end{coq_example*}
-
-\begin{Variants}
- \item {\tt jp $n$}\\
-   \tacindex{jp $n$} 
-   Tries the {\em Jprover} procedure with multiplicities up to $n$,
-   starting from 1.
- \item {\tt jp}\\
-   Tries the {\em Jprover} procedure without multiplicity bound, 
-   possibly running forever.
-\end{Variants}
-
-\begin{ErrMsgs}
- \item \errindex{multiplicity limit reached}\\
-   The procedure tried all multiplicities below the limit and
-   failed. Goal might be solved by increasing the multiplicity limit. 
- \item \errindex{formula is not provable}\\
-   The procedure determined that goal was not provable in
-   intuitionistic first-order logic, no matter how big the
-   multiplicity is.
-\end{ErrMsgs}
+%% \subsection{{\tt jp} {\em (Jprover)}
+%% \tacindex{jp}
+%% \label{jprover}}
+
+%% The tactic \texttt{jp}, due to Huang Guan-Shieng, is an experimental
+%% port of the {\em Jprover}\cite{SLKN01} semi-decision procedure for
+%% first-order intuitionistic logic implemented in {\em
+%%   NuPRL}\cite{Kre02}.
+
+%% The tactic \texttt{jp}, due to Huang Guan-Shieng, is an {\it
+%%   experimental} port of the {\em Jprover}\cite{SLKN01} semi-decision 
+%% procedure for first-order intuitionistic logic implemented in {\em
+%%   NuPRL}\cite{Kre02}. 
+
+%% Search may optionnaly be bounded by a multiplicity parameter
+%% indicating how many (at most) copies of a formula may be used in 
+%% the proof process, its absence may lead to non-termination of the tactic.
+
+%% %\begin{coq_eval}
+%% %Variable S:Set.
+%% %Variables P Q:S->Prop.
+%% %Variable f:S->S.
+%% %\end{coq_eval}
+
+%% %\begin{coq_example*}
+%% %Lemma example: (exists x |P x\/Q x)->(exists x |P x)\/(exists x |Q x).
+%% %jp.
+%% %Qed.
+
+%% %Lemma example2: (forall x ,P x->P (f x))->forall x,P x->P (f(f x)).
+%% %jp.
+%% %Qed.
+%% %\end{coq_example*}
+
+%% \begin{Variants}
+%%  \item {\tt jp $n$}\\
+%%    \tacindex{jp $n$} 
+%%    Tries the {\em Jprover} procedure with multiplicities up to $n$,
+%%    starting from 1.
+%%  \item {\tt jp}\\
+%%    Tries the {\em Jprover} procedure without multiplicity bound, 
+%%    possibly running forever.
+%% \end{Variants}
+
+%% \begin{ErrMsgs}
+%%  \item \errindex{multiplicity limit reached}\\
+%%    The procedure tried all multiplicities below the limit and
+%%    failed. Goal might be solved by increasing the multiplicity limit. 
+%%  \item \errindex{formula is not provable}\\
+%%    The procedure determined that goal was not provable in
+%%    intuitionistic first-order logic, no matter how big the
+%%    multiplicity is.
+%% \end{ErrMsgs}
 
 
 % \subsection{\tt Linear}\tacindex{Linear}\label{Linear}
@@ -2303,7 +2303,7 @@ congruence closure algorithm, which is a decision procedure for ground
 equalities with uninterpreted symbols. It also include the constructor theory
 (see \ref{injection} and \ref{discriminate}).
 If the goal is a non-quantified equality, {\tt congruence} tries to
-prove it with non-quantified equalities in the constext. Otherwise it
+prove it with non-quantified equalities in the context. Otherwise it
 tries to infer a discriminable equality from those in the context.
 
 \begin{coq_eval}
@@ -2335,11 +2335,11 @@ congruence.
 \end{coq_example}
 
 \begin{ErrMsgs}
-  \item \errindex{I don't know how to handle dependent equality}
+  \item \errindex{I don't know how to handle dependent equality} \\
     The decision procedure managed to find a proof of the goal or of
     a discriminable equality but this proof couldn't be built in Coq
     because of dependently-typed functions.
-  \item \errindex{I couldn't solve goal}
+  \item \errindex{I couldn't solve goal} \\
     The decision procedure didn't managed to find a proof of the goal or of
     a discriminable equality.
 \end{ErrMsgs}
diff --git a/doc/biblio.bib b/doc/biblio.bib
index 866f30686..a91264311 100755
--- a/doc/biblio.bib
+++ b/doc/biblio.bib
@@ -691,16 +691,6 @@ Alan Robinson},
         YEAR               = {1952}
 }
 
-@MANUAL{Kre02,
-        AUTHOR             = {C. Kreitz},
-        TITLE              = {The Nuprl Proof Development System, Version 5~:
-Reference Manual and User's Guide},
-        INSTITUTION        = {Department of Computer Science, 
-Cornell University},
-        MONTH              = dec,
-        YEAR               = {2002}
-} 
-
 @BOOK{Kri90,
         AUTHOR             = {J.-L. Krivine},
         PUBLISHER          = {Masson},
@@ -939,21 +929,6 @@ the Calculus of Inductive Constructions}},
         YEAR               = {1994}
 }
 
-@INPROCEEDINGS{SLKN01,
-        AUTHOR             = {S. Schmitt and L. Lorigo and C. Kreitz 
-and A. Nogin},
-        TITLE              = {Integrating Connection-based Theorem Proving 
-into Interactive Proof Assistants}, 
-        BOOKTITLE          = {Proceedings of International Joint Conference on 
-Automated Reasoning},
-        EDITOR             = {R. Gore and A. Leitsch and T. Nipkow},
-        PUBLISHER          = SV,
-        SERIES             = LNAI,
-        VOLUME             = {2083},
-        PAGES              = {421--426},
-        YEAR               = {2001}
-}
-
 
 @MASTERSTHESIS{Ter92,
         AUTHOR             = {D. Terrasse},