aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/inductive.ml4
-rw-r--r--kernel/cbytegen.ml12
-rw-r--r--kernel/inductive.ml4
-rw-r--r--lib/cArray.ml1
-rw-r--r--lib/cArray.mli1
-rw-r--r--plugins/cc/ccalgo.ml4
-rw-r--r--plugins/extraction/modutil.ml2
-rw-r--r--plugins/nsatz/nsatz.ml42
-rw-r--r--plugins/nsatz/polynom.ml12
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/indrec.ml4
-rw-r--r--pretyping/termops.ml4
-rw-r--r--toplevel/auto_ind_decl.ml4
13 files changed, 27 insertions, 29 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 605405e35..b04c77ad8 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -525,8 +525,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
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
diff --git a/lib/cArray.ml b/lib/cArray.ml
index a5e38534f..7ffdeb6a1 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -12,7 +12,6 @@ sig
external get : 'a array -> int -> 'a = "%array_safe_get"
external set : 'a array -> int -> 'a -> unit = "%array_safe_set"
external make : int -> 'a -> 'a array = "caml_make_vect"
- external create : int -> 'a -> 'a array = "caml_make_vect"
val init : int -> (int -> 'a) -> 'a array
val make_matrix : int -> int -> 'a -> 'a array array
val create_matrix : int -> int -> 'a -> 'a array array
diff --git a/lib/cArray.mli b/lib/cArray.mli
index 57eb672c1..ed8a1e94c 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -14,7 +14,6 @@ sig
external get : 'a array -> int -> 'a = "%array_safe_get"
external set : 'a array -> int -> 'a -> unit = "%array_safe_set"
external make : int -> 'a -> 'a array = "caml_make_vect"
- external create : int -> 'a -> 'a array = "caml_make_vect"
val init : int -> (int -> 'a) -> 'a array
val make_matrix : int -> int -> 'a -> 'a array array
val create_matrix : int -> int -> 'a -> 'a array array
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index f029c053a..21077ecc8 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -241,7 +241,7 @@ let empty depth gls:state =
{uf=
{max_size=init_size;
size=0;
- map=Array.create init_size dummy_node;
+ map=Array.make init_size dummy_node;
epsilons=[];
axioms=Constrhash.create init_size;
syms=Termhash.create init_size};
@@ -335,7 +335,7 @@ let next uf=
let nsize= succ size in
if nsize=uf.max_size then
let newmax=uf.max_size * 3 / 2 + 1 in
- let newmap=Array.create newmax dummy_node in
+ let newmap=Array.make newmax dummy_node in
begin
uf.max_size<-newmax;
Array.blit uf.map 0 newmap 0 size;
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 0ed6a2855..43a08657b 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -358,7 +358,7 @@ let rec depcheck_se = function
(* Hack to avoid extracting unused part of a Dfix *)
match d with
| Dfix (rv,trms,tys) when (List.for_all is_custom refs') ->
- let trms' = Array.create (Array.length rv) (MLexn "UNUSED") in
+ let trms' = Array.make (Array.length rv) (MLexn "UNUSED") in
((l,SEdecl (Dfix (rv,trms',tys))) :: se')
| _ -> (compute_deps_decl d; t::se')
end
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 34be7244d..7b42fc5ba 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -427,7 +427,7 @@ let remove_list_tail l i =
let remove_zeros zero lci =
let n = List.length (List.hd lci) in
let m=List.length lci in
- let u = Array.create m false in
+ let u = Array.make m false in
let rec utiles k =
if k>=m
then ()
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index a610c8461..ce70a0ffb 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -133,7 +133,7 @@ let x n = Prec (n,[|cf0;cf1|])
let monome v n =
match n with
0->Pint coef1;
- |_->let tmp = Array.create (n+1) (Pint coef0) in
+ |_->let tmp = Array.make (n+1) (Pint coef0) in
tmp.(n)<-(Pint coef1);
Prec (v, tmp)
@@ -191,7 +191,7 @@ let norm p = match p with
if !n<0 then Pint coef0
else if !n=0 then a.(0)
else if !n=d then p
- else (let b=Array.create (!n+1) (Pint coef0) in
+ else (let b=Array.make (!n+1) (Pint coef0) in
for i=0 to !n do b.(i)<-a.(i);done;
Prec(x,b))
@@ -243,7 +243,7 @@ let rec plusP p q =
Prec (x,p2))
else
(let n=max (deg x p) (deg x q) in
- let r=Array.create (n+1) (Pint coef0) in
+ let r=Array.make (n+1) (Pint coef0) in
for i=0 to n do
r.(i)<- plusP (coef x i p) (coef x i q);
done;
@@ -277,13 +277,13 @@ let rec vars=function
(* multiply p by v^n, v >= max_var p *)
let multx n v p =
match p with
- Prec (x,p1) when x=v -> let p2= Array.create ((Array.length p1)+n) (Pint coef0) in
+ Prec (x,p1) when x=v -> let p2= Array.make ((Array.length p1)+n) (Pint coef0) in
for i=0 to (Array.length p1)-1 do
p2.(i+n)<-p1.(i);
done;
Prec (x,p2)
|_ -> if equal p (Pint coef0) then (Pint coef0)
- else (let p2=Array.create (n+1) (Pint coef0) in
+ else (let p2=Array.make (n+1) (Pint coef0) in
p2.(n)<-p;
Prec (v,p2))
@@ -320,7 +320,7 @@ let deriv v p =
let d = Array.length p1 -1 in
if d=1 then p1.(1)
else
- (let p2 = Array.create d (Pint coef0) in
+ (let p2 = Array.make d (Pint coef0) in
for i=0 to d-1 do
p2.(i)<- multP (Pint (coef_of_int (i+1))) p1.(i+1);
done;
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 71c9325d7..bcf4b9e4a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1092,7 +1092,7 @@ let first_clause_irrefutable env = function
let group_equations pb ind current cstrs mat =
let mat =
if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in
- let brs = Array.create (Array.length cstrs) [] in
+ let brs = Array.make (Array.length cstrs) [] in
let only_default = ref true in
let _ =
List.fold_right (* To be sure it's from bottom to top *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index b01a463a1..9c08a8bf6 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -270,7 +270,7 @@ let mis_make_indrec env sigma listdepkind mib =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let nrec = List.length listdepkind in
let depPvec =
- Array.create mib.mind_ntypes (None : (bool * constr) option) in
+ Array.make mib.mind_ntypes (None : (bool * constr) option) in
let _ =
let rec
assign k = function
@@ -380,7 +380,7 @@ let mis_make_indrec env sigma listdepkind mib =
let fixn = Array.of_list (List.rev ln) in
let fixtyi = Array.of_list (List.rev ltyp) in
let fixdef = Array.of_list (List.rev ldef) in
- let names = Array.create nrec (Name(Id.of_string "F")) in
+ let names = Array.make nrec (Name(Id.of_string "F")) in
mkFix ((fixn,p),(names,fixtyi,fixdef))
in
mrec 0 [] [] []
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f5be89689..70843c7a9 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -343,8 +343,8 @@ let fold_rec_types g (lna,typarray,_) e =
let map_left2 f a g b =
let l = Array.length a in
if Int.equal l 0 then [||], [||] else begin
- let r = Array.create l (f a.(0)) in
- let s = Array.create l (g b.(0)) in
+ let r = Array.make l (f a.(0)) in
+ let s = Array.make l (g b.(0)) in
for i = 1 to l - 1 do
r.(i) <- f a.(i);
s.(i) <- g b.(i)
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 5ef789561..20c02878a 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -227,10 +227,10 @@ let build_beq_scheme kn =
extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in
let constrsi = constrs (3+nparrec) in
let n = Array.length constrsi in
- let ar = Array.create n ff in
+ let ar = Array.make n ff in
for i=0 to n-1 do
let nb_cstr_args = List.length constrsi.(i).cs_args in
- let ar2 = Array.create n ff in
+ let ar2 = Array.make n ff in
let constrsj = constrs (3+nparrec+nb_cstr_args) in
for j=0 to n-1 do
if Int.equal i j then
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 15:14:55 +0000