diff options
| author | herbelin | 2004-12-29 12:14:31 +0000 |
|---|---|---|
| committer | herbelin | 2004-12-29 12:14:31 +0000 |
| commit | bcd079c448c946270cbf3c5323ac8cf185450b5f (patch) | |
| tree | 28c7e443cf77af53d6b751543e2c6a061758dc03 | |
| parent | 2f28a6c3368c6589affce381efd7946a86de5f46 (diff) | |
Bug control_only_guard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6524 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/inductiveops.ml | 6 |
1 files 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 |