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

2 files changed, 28 insertions, 25 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index aeae4fa2c..e292013db 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.
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 69f921b79..f7d084382 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -393,31 +393,16 @@ let arity_of_case_predicate env (ind,params) dep k =
 (* A function which checks that a term well typed verifies both
    syntactic conditions *)
 
-let control_only_guard env = 
-  let rec control_rec c = match kind_of_term c with
-    | Rel _ | Var _    -> ()
-    | Sort _ | Meta _ -> ()
-    | Ind _       -> ()
-    | Construct _ -> ()
-    | Const _        -> ()
-    | CoFix (_,(_,tys,bds) as cofix) ->
-	Inductive.check_cofix env cofix;
-	Array.iter control_rec tys;
-	Array.iter control_rec bds;
-    | Fix (_,(_,tys,bds) as fix) ->
-	Inductive.check_fix env fix; 
-	Array.iter control_rec tys;
-	Array.iter control_rec bds;
-    | Case(_,p,c,b) -> control_rec p;control_rec c;Array.iter control_rec b
-    | Evar (_,cl)        -> Array.iter control_rec cl
-    | App (c,cl)         -> control_rec c; Array.iter control_rec cl
-    | Cast (c1,_, c2)  -> control_rec c1; control_rec c2
-    | Prod (_,c1,c2)     -> control_rec c1; control_rec c2
-    | Lambda (_,c1,c2)   -> control_rec c1; control_rec c2
-    | LetIn (_,c1,c2,c3) -> control_rec c1; control_rec c2; control_rec c3
+let control_only_guard env c = 
+  let check_fix_cofix e c = match kind_of_term c with
+    | CoFix (_,(_,_,_) as cofix) ->
+	Inductive.check_cofix e cofix
+    | Fix (_,(_,_,_) as fix) ->
+	Inductive.check_fix e fix
+    | _ -> ()
   in 
-  control_rec 
-
+    iter_constr_with_full_binders push_rel check_fix_cofix env c
+   
 let subst_inductive subst (kn,i as ind) = 
   let kn' = Mod_subst.subst_kn subst kn in
   if kn == kn' then ind else (kn',i)