diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -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 24a8fbc7..c33a261b 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductiveops.ml,v 1.14.2.1 2004/07/16 19:30:45 herbelin Exp $ *) +(* $Id: inductiveops.ml,v 1.14.2.2 2004/12/29 12:15:00 herbelin Exp $ *) open Util open Names @@ -341,9 +341,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 + | 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 + | 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 |