Modification de control_only_guard, qui utilise maintenant

iter_constr_with_full_binders + documentation de Guarded.

 --Cette ligne, et les suivantes ci-dessous, seront ignorées--

M    trunk/doc/refman/RefMan-pro.tex
M    trunk/pretyping/inductiveops.ml


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

1 files changed, 19 insertions, 1 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index aeae4fa2ca..e292013db4 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -299,7 +299,7 @@ This focuses the attention on the $\num^{\scriptsize th}$ subgoal to prove.
 Turns off the focus mode.
 
 
-\section{Displaying information}
+\section{Requesting information}
 
 \subsection[\tt Show.]{\tt Show.\comindex{Show}\label{Show}}
 This command displays the current goals.
@@ -378,15 +378,33 @@ along with the type and the context of each variable.
 
 \end{Variants}
 
+
+\subsection[\tt Guarded.]
+
+Some tactics (e.g. refine \ref{refine}) allow to build proofs using
+fixpoint or co-fixpoint constructions. Due to the incremental nature
+of interactive proof construction, the check of the termination (or
+guardedness) of the recursive calls in the fixpoint or cofixpoint
+constructions is postponed to the time of the completion of the proof.
+
+The command \verb!Guarded! allows to verify if the guard condition for
+fixpoint and cofixpoint is violated at some time of the construction
+of the proof without having to wait the completion of the proof."
+
+
 \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. 
 All the hypotheses remains usable in the proof development.
 
+
 \subsection[\tt Unset Hyps Limit.]{\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.