summaryrefslogtreecommitdiff
path: root/pretyping/inductiveops.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-01-31 14:34:14 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-01-31 14:34:14 +0000
commit6497f27021fec4e01f2182014f2bb1989b4707f9 (patch)
tree473be7e63895a42966970ab6a70998113bc1bd59 /pretyping/inductiveops.ml
parent6b649aba925b6f7462da07599fe67ebb12a3460e (diff)
Imported Upstream version 8.0pl2upstream/8.0pl2
Diffstat (limited to 'pretyping/inductiveops.ml')
-rw-r--r--pretyping/inductiveops.ml6
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