diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-19 00:13:21 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-19 00:13:21 +0000 |
| commit | 32b7a0cc9c8302febd7639d22c80554fa4ec8d88 (patch) | |
| tree | c5798518db283d05d83d399802c5d50b093b417f /kernel | |
| parent | 7a30e5bbcfb2dc3e7b7bf0cf2cd4e27eab31dcfb (diff) | |
Array.create is deprecated
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16104 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cbytegen.ml | 12 | ||||
| -rw-r--r-- | kernel/inductive.ml | 4 |
2 files changed, 8 insertions, 8 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 021e50847..d0751475b 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -537,8 +537,8 @@ let rec compile_constr reloc c sz cont = | Fix ((rec_args,init),(_,type_bodies,rec_bodies)) -> let ndef = Array.length type_bodies in let rfv = ref empty_fv in - let lbl_types = Array.create ndef Label.no in - let lbl_bodies = Array.create ndef Label.no in + let lbl_types = Array.make ndef Label.no in + let lbl_bodies = Array.make ndef Label.no in (* Compilation des types *) let env_type = comp_env_fix_type rfv in for i = 0 to ndef - 1 do @@ -566,8 +566,8 @@ let rec compile_constr reloc c sz cont = | CoFix(init,(_,type_bodies,rec_bodies)) -> let ndef = Array.length type_bodies in - let lbl_types = Array.create ndef Label.no in - let lbl_bodies = Array.create ndef Label.no in + let lbl_types = Array.make ndef Label.no in + let lbl_bodies = Array.make ndef Label.no in (* Compiling types *) let rfv = ref empty_fv in let env_type = comp_env_cofix_type ndef rfv in @@ -600,8 +600,8 @@ let rec compile_constr reloc c sz cont = let mib = lookup_mind (fst ind) !global_env in let oib = mib.mind_packets.(snd ind) in let tbl = oib.mind_reloc_tbl in - let lbl_consts = Array.create oib.mind_nb_constant Label.no in - let lbl_blocks = Array.create (oib.mind_nb_args+1) Label.no in + let lbl_consts = Array.make oib.mind_nb_constant Label.no in + let lbl_blocks = Array.make (oib.mind_nb_args+1) Label.no in let branch1,cont = make_branch cont in (* Compiling return type *) let lbl_typ,fcode = diff --git a/kernel/inductive.ml b/kernel/inductive.ml index dddac2ba0..740ac8c13 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -522,8 +522,8 @@ let branches_specif renv c_spec ci = Array.map (fun t -> Lazy.force (spec_of_tree (lazy t))) vra - | Dead_code -> Array.create nca Dead_code - | _ -> Array.create nca Not_subterm) in + | Dead_code -> Array.make nca Dead_code + | _ -> Array.make nca Not_subterm) in List.tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca) car |