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 +++++++---
 test-suite/failure/fixpoint2.v |  6 ++++++
 2 files changed, 13 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/failure/fixpoint2.v

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)
diff --git a/test-suite/failure/fixpoint2.v b/test-suite/failure/fixpoint2.v
new file mode 100644
index 0000000000..d2f02ea138
--- /dev/null
+++ b/test-suite/failure/fixpoint2.v
@@ -0,0 +1,6 @@
+(* Check Guard in proofs *)
+
+Goal nat->nat.
+fix f 1.
+intro n; apply f; assumption.
+Guarded.
-- 
cgit v1.2.3