diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d86abb435f..81e6c8f170 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -779,7 +779,7 @@ let check_one_fix renv recpos def = check_rec_call renv [] def let judgment_of_fixpoint (_, types, bodies) = - array_map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies + Array.map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = let nbfix = Array.length bodies in @@ -815,7 +815,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = | _ -> raise_err env i NotEnoughAbstractionInFixBody in check_occur fixenv 1 def in (* Do it on every fixpoint *) - let rv = array_map2_i find_ind nvect bodies in + let rv = Array.map2_i find_ind nvect bodies in (Array.map fst rv, Array.map snd rv) @@ -898,7 +898,7 @@ let check_one_cofix env nbfix def deftype = if (List.for_all (noccur_with_meta n nbfix) args) then let nbfix = Array.length vdefs in - if (array_for_all (noccur_with_meta n nbfix) varit) then + if (Array.for_all (noccur_with_meta n nbfix) varit) then let env' = push_rec_types recdef env in (Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs; List.iter (check_rec_call env alreadygrd n vlra) args) |