From cea1b255c95d9fa6cc6c2a391c50e9280066fd8c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Sep 2007 07:36:14 +0000
Subject: Itération sur les sous-termes dans la vérification de la condition de
 garde

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10114 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/inductiveops.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index f7d0843822..66f3456439 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -400,9 +400,13 @@ let control_only_guard env c =
     | Fix (_,(_,_,_) as fix) ->
 	Inductive.check_fix e fix
     | _ -> ()
-  in 
-    iter_constr_with_full_binders push_rel check_fix_cofix env c
-   
+  in
+  let rec iter env c = 
+    check_fix_cofix env c; 
+    iter_constr_with_full_binders push_rel iter env c
+  in
+  iter 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)
-- 
cgit v1.2.3