From bcd079c448c946270cbf3c5323ac8cf185450b5f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 29 Dec 2004 12:14:31 +0000
Subject: Bug control_only_guard

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

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index c03dab08be..cda1169dd7 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -342,9 +342,9 @@ let control_only_guard env =
 	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 (_,cl)         -> Array.iter control_rec cl
+    | 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
-- 
cgit v1.2.3