aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/indtypes.ml6
-rw-r--r--checker/inductive.ml4
-rw-r--r--kernel/indtypes.ml6
-rw-r--r--kernel/inductive.ml4
-rw-r--r--lib/cArray.ml46
-rw-r--r--lib/cList.ml67
-rw-r--r--lib/cList.mli6
-rw-r--r--library/heads.ml2
-rw-r--r--plugins/cc/cctac.ml2
-rw-r--r--plugins/decl_mode/decl_interp.ml5
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml2
-rw-r--r--plugins/firstorder/instances.ml2
-rw-r--r--plugins/firstorder/rules.ml2
-rw-r--r--plugins/firstorder/sequent.ml4
-rw-r--r--plugins/firstorder/unify.ml2
-rw-r--r--plugins/setoid_ring/newring.ml42
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/detyping.ml4
-rw-r--r--pretyping/indrec.ml2
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--printing/printer.ml2
-rw-r--r--tactics/auto.ml7
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/tactics.ml4
-rw-r--r--toplevel/discharge.ml2
-rw-r--r--toplevel/indschemes.ml2
-rw-r--r--toplevel/obligations.ml2
29 files changed, 89 insertions, 112 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 9a669e403..8f93ff0be 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -355,8 +355,8 @@ let abstract_mind_lc env ntyps npars lc =
lc
else
let make_abs =
- List.tabulate
- (function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps
+ List.init ntyps
+ (function i -> lambda_implicit_lift npars (Rel (i+1)))
in
Array.map (substl make_abs) lc
@@ -514,7 +514,7 @@ let check_positivity env_ar mind params nrecp inds =
let lparams = rel_context_length params in
let check_one i mip =
let ra_env =
- List.tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
+ List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
in
diff --git a/checker/inductive.ml b/checker/inductive.ml
index abc162af7..5fdca0fab 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -58,7 +58,7 @@ let inductive_params (mib,_) = mib.mind_nparams
let ind_subst mind mib =
let ntypes = mib.mind_ntypes in
let make_Ik k = Ind (mind,ntypes-k-1) in
- List.tabulate make_Ik ntypes
+ List.init ntypes make_Ik
(* Instantiate inductives in constructor type *)
let constructor_instantiate mind mib c =
@@ -527,7 +527,7 @@ let branches_specif renv c_spec ci =
vra
| Dead_code -> Array.make nca Dead_code
| _ -> Array.make nca Not_subterm) in
- List.tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
+ List.init nca (fun j -> lazy (Lazy.force lvra).(j)))
car
(* [subterm_specif renv t] computes the recursive structure of [t] and
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e6faaaa85..57e638982 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -386,8 +386,8 @@ let abstract_mind_lc env ntyps npars lc =
lc
else
let make_abs =
- List.tabulate
- (function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps
+ List.init ntyps
+ (function i -> lambda_implicit_lift npars (mkRel (i+1)))
in
Array.map (substl make_abs) lc
@@ -552,7 +552,7 @@ let check_positivity kn env_ar params inds =
let nmr = rel_context_nhyps params in
let check_one i (_,lcnames,lc,(sign,_)) =
let ra_env =
- List.tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
+ List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
let nargs = rel_context_nhyps sign - nmr in
check_positivity_one ienv params (kn,i) nargs lcnames lc
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 3132b7e79..b93237679 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -55,7 +55,7 @@ let inductive_params (mib,_) = mib.mind_nparams
let ind_subst mind mib =
let ntypes = mib.mind_ntypes in
let make_Ik k = mkInd (mind,ntypes-k-1) in
- List.tabulate make_Ik ntypes
+ List.init ntypes make_Ik
(* Instantiate inductives in constructor type *)
let constructor_instantiate mind mib c =
@@ -527,7 +527,7 @@ let branches_specif renv c_spec ci =
vra
| Dead_code -> Array.make nca Dead_code
| _ -> Array.make nca Not_subterm) in
- List.tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
+ List.init nca (fun j -> lazy (Lazy.force lvra).(j)))
car
(* [subterm_specif renv t] computes the recursive structure of [t] and
diff --git a/lib/cArray.ml b/lib/cArray.ml
index 05c8cc87c..eff317aac 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -90,31 +90,43 @@ include Array
(* Arrays *)
-let compare item_cmp v1 v2 =
- let c = compare (Array.length v1) (Array.length v2) in
- if c<>0 then c else
- let rec cmp = function
- -1 -> 0
- | i ->
- let c' = item_cmp v1.(i) v2.(i) in
- if c'<>0 then c'
- else cmp (i-1) in
- cmp (Array.length v1 - 1)
+let compare cmp v1 v2 =
+ if v1 == v2 then 0
+ else
+ let len = Array.length v1 in
+ let c = Int.compare len (Array.length v2) in
+ if c <> 0 then c else
+ let rec loop i =
+ if i < 0 then 0
+ else
+ let x = Array.unsafe_get v1 i in
+ let y = Array.unsafe_get v2 i in
+ let c = cmp x y in
+ if c <> 0 then c
+ else loop (i - 1)
+ in
+ loop (len - 1)
let equal cmp t1 t2 =
if t1 == t2 then true else
- if not (Array.length t1 = Array.length t2) then false
- else
- let rec aux i =
- (i = Array.length t1) || (cmp t1.(i) t2.(i) && aux (i + 1))
- in aux 0
+ let len = Array.length t1 in
+ if not (Int.equal len (Array.length t2)) then false
+ else
+ let rec aux i =
+ if i < 0 then true
+ else
+ let x = Array.unsafe_get t1 i in
+ let y = Array.unsafe_get t2 i in
+ cmp x y && aux (pred i)
+ in
+ aux (len - 1)
-let is_empty array = (Array.length array) = 0
+let is_empty array = Int.equal (Array.length array) 0
let exists f v =
let rec exrec = function
| -1 -> false
- | n -> (f v.(n)) || (exrec (n-1))
+ | n -> f (Array.unsafe_get v n) || (exrec (n-1))
in
exrec ((Array.length v)-1)
diff --git a/lib/cList.ml b/lib/cList.ml
index 8e031a0c9..e3d5f080b 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -57,6 +57,7 @@ sig
val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
val is_empty : 'a list -> bool
+ val init : int -> (int -> 'a) -> 'a list
val add_set : 'a -> 'a list -> 'a list
val eq_set : 'a list -> 'a list -> bool
val intersect : 'a list -> 'a list -> 'a list
@@ -64,9 +65,6 @@ sig
val unionq : 'a list -> 'a list -> 'a list
val subtract : 'a list -> 'a list -> 'a list
val subtractq : 'a list -> 'a list -> 'a list
-
- (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *)
- val tabulate : (int -> 'a) -> int -> 'a list
val interval : int -> int -> int list
val make : int -> 'a -> 'a list
val assign : 'a list -> int -> 'a -> 'a list
@@ -76,9 +74,6 @@ sig
val map_filter : ('a -> 'b option) -> 'a list -> 'b list
val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
val filter_with : bool list -> 'a list -> 'a list
-
- (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i
- [ f ai == ai], then [smartmap f l==l] *)
val smartmap : ('a -> 'a) -> 'a list -> 'a list
val map_left : ('a -> 'b) -> 'a list -> 'b list
val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
@@ -90,19 +85,10 @@ sig
('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
val filteri :
(int -> 'a -> bool) -> 'a list -> 'a list
-
- (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
- [f ai = true], then [smartfilter f l==l] *)
val smartfilter : ('a -> bool) -> 'a list -> 'a list
-
- (** [index] returns the 1st index of an element in a list (counting from 1) *)
val index : 'a -> 'a list -> int
val index_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
-
- (** [unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
val unique_index : 'a -> 'a list -> int
-
- (** [index0] behaves as [index] except that it starts counting at 0 *)
val index0 : 'a -> 'a list -> int
val index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
val iteri : (int -> 'a -> unit) -> 'a list -> unit
@@ -121,12 +107,9 @@ sig
val sep_last : 'a list -> 'a * 'a list
val find_map : ('a -> 'b option) -> 'a list -> 'b
val uniquize : 'a list -> 'a list
-
- (** merges two sorted lists and preserves the uniqueness property: *)
val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
val subset : 'a list -> 'a list -> bool
val chop : int -> 'a list -> 'a list * 'a list
- (* former [split_at] was a duplicate of [chop] *)
val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
val firstn : int -> 'a list -> 'a list
@@ -136,42 +119,21 @@ sig
val skipn_at_least : int -> 'a list -> 'a list
val addn : int -> 'a -> 'a list -> 'a list
val prefix_of : 'a list -> 'a list -> bool
-
- (** [drop_prefix p l] returns [t] if [l=p++t] else return [l] *)
val drop_prefix : 'a list -> 'a list -> 'a list
val drop_last : 'a list -> 'a list
-
- (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
val map_append : ('a -> 'b list) -> 'a list -> 'b list
-
- (** raises [Invalid_argument] if the two lists don't have the same length *)
val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
-
- (** [fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
- where [(e_i,k_i)=f e_{i-1} l_i] *)
val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
val assoc_f : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b
-
- (** A generic cartesian product: for any operator (**),
- [cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
- and so on if there are more elements in the lists. *)
val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
-
- (** [cartesians] is an n-ary cartesian product: it iterates
- [cartesian] over a list of lists. *)
val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
-
- (** combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
val combinations : 'a list list -> 'a list list
val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
-
val cartesians_filter :
('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
- (** Keep only those products that do not return None *)
-
val factorize_left : ('a * 'b) list -> ('a * 'b list) list
end
@@ -239,6 +201,21 @@ let rec copy p = function
p.tail <- cast c;
copy c l
+let rec init_loop len f p i =
+ if Int.equal i len then ()
+ else
+ let c = { head = f i; tail = [] } in
+ p.tail <- cast c;
+ init_loop len f c (succ i)
+
+let init len f =
+ if len < 0 then invalid_arg "List.init"
+ else if Int.equal len 0 then []
+ else
+ let c = { head = f 0; tail = [] } in
+ init_loop len f c 1;
+ cast c
+
let rec concat_loop p = function
| [] -> ()
| x :: l -> concat_loop (copy p x) l
@@ -362,17 +339,7 @@ let subtract l1 l2 =
let subtractq l1 l2 =
if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1
-let rec tabulate_loop f len p i =
- if len <= i then ()
- else
- let c = { head = f i; tail = [] } in
- let () = p.tail <- cast c in
- tabulate_loop f len c (succ i)
-
-let tabulate f len =
- let dummy = { head = Obj.magic 0; tail = [] } in
- tabulate_loop f len dummy 0;
- dummy.tail
+let tabulate = init
let interval n m =
let rec interval_n (l,m) =
diff --git a/lib/cList.mli b/lib/cList.mli
index 9b3a988ab..af378a37f 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -66,6 +66,9 @@ sig
val is_empty : 'a list -> bool
(** Checks whether a list is empty *)
+ val init : int -> (int -> 'a) -> 'a list
+ (** [init n f] constructs the list [f 0; ... ; f (n - 1)]. *)
+
val add_set : 'a -> 'a list -> 'a list
(** [add_set x l] adds [x] in [l] if it is not already there, or returns [l]
otherwise. *)
@@ -79,9 +82,6 @@ sig
val subtract : 'a list -> 'a list -> 'a list
val subtractq : 'a list -> 'a list -> 'a list
- val tabulate : (int -> 'a) -> int -> 'a list
- (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *)
-
val interval : int -> int -> int list
(** [interval i j] creates the list [[i; i + 1; ...; j]], or [[]] when
[j <= i]. *)
diff --git a/library/heads.ml b/library/heads.ml
index 62e27dd00..e6c9bc9a8 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -119,7 +119,7 @@ let kind_of_head env t =
else
(* enough arguments to [cst] *)
k,List.skipn n l,List.nth l (i-1) in
- let l' = List.tabulate (fun _ -> mkMeta 0) q @ rest in
+ let l' = List.make q (mkMeta 0) @ rest in
aux k' l' a (with_subcase or with_case)
| ConstructorHead when with_case -> NotImmediatelyComputableHead
| x -> x
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 20cf9edb8..a5baa00f9 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -365,7 +365,7 @@ let discriminate_tac cstr p gls =
let build_term_to_complete uf meta pac =
let cinfo = get_constructor_info uf pac.cnode in
let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
- let dummy_args = List.rev (List.tabulate meta pac.arity) in
+ let dummy_args = List.rev (List.init pac.arity meta) in
let all_args = List.rev_append real_args dummy_args in
applistc (mkConstruct cinfo.ci_constr) all_args
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 3cc0686ad..9d34dc99a 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -341,9 +341,8 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
(fun (loc,(id,_)) ->
GVar (loc,id)) params in
let dum_args=
- List.tabulate
- (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false)))
- oib.Declarations.mind_nrealargs in
+ List.init oib.Declarations.mind_nrealargs
+ (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false))) in
glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in
let pat_vars,aliases,patt = interp_pattern env pat in
let inject = function
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 1ae8419c8..2ef2c9756 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1190,7 +1190,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
match List.assoc id args with
[None,br_args] ->
let all_metas =
- List.tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in
+ List.init (nparams + nhyps) (fun n -> mkMeta (succ n)) in
let param_metas,hyp_metas = List.chop nparams all_metas in
tclTHEN
(tclDO nhrec introf)
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index baf1972e6..12b2304ac 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -112,7 +112,7 @@ let mk_open_instance id gl m t=
match nam with
Name id -> id
| Anonymous -> dummy_bvid in
- let revt=substl (List.tabulate (fun i->mkRel (m-i)) m) t in
+ let revt=substl (List.init m (fun i->mkRel (m-i))) t in
let rec aux n avoid=
if n=0 then [] else
let nid=(fresh_id avoid var_id gl) in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index c812deaf5..8abf9d7e2 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -129,7 +129,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
it_mkLambda_or_LetIn head rc in
let lp=Array.length rcs in
- let newhyps=List.tabulate myterm lp in
+ let newhyps=List.init lp myterm in
tclIFTHENELSE
(tclTHENLIST
[generalize newhyps;
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 238813e39..4e4a6f19f 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -189,8 +189,8 @@ let empty_seq depth=
let expand_constructor_hints =
List.map_append (function
| IndRef ind ->
- List.tabulate (fun i -> ConstructRef (ind,i+1))
- (Inductiveops.nconstructors ind)
+ List.init (Inductiveops.nconstructors ind)
+ (fun i -> ConstructRef (ind,i+1))
| gr ->
[gr])
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 93f84687e..75fd0261a 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -124,7 +124,7 @@ let unif_atoms i dom t1 t2=
| Not_found ->Some (Phantom dom)
let renum_metas_from k n t= (* requires n = max (free_rels t) *)
- let l=List.tabulate (fun i->mkMeta (k+i)) n in
+ let l=List.init n (fun i->mkMeta (k+i)) in
substl l t
let more_general (m1,t1) (m2,t2)=
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index a0f565ce3..1b2ba0e87 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -179,7 +179,7 @@ let dummy_goal env =
Evd.sigma = sigma}
let exec_tactic env n f args =
- let lid = List.tabulate(fun i -> Id.of_string("x"^string_of_int i)) n in
+ let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
let res = ref [||] in
let get_res ist =
let l = List.map (fun id -> List.assoc id ist.lfun) lid in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 9c61d3f06..7d2ad487c 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -52,7 +52,7 @@ let apply_pattern_coercion loc pat p =
List.fold_left
(fun pat (co,n) ->
let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in
- Glob_term.PatCstr (loc, co, List.tabulate f (n+1), Anonymous))
+ Glob_term.PatCstr (loc, co, List.init (n+1) f, Anonymous))
pat p
(* raise Not_found if no coercion found *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 89e6bf822..cc900adb4 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -240,8 +240,8 @@ let rec build_tree na isgoal e ci cl =
let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in
let cnl = ci.ci_cstr_ndecls in
List.flatten
- (List.tabulate (fun i -> contract_branch isgoal e (cnl.(i),mkpat i,cl.(i)))
- (Array.length cl))
+ (List.init (Array.length cl)
+ (fun i -> contract_branch isgoal e (cnl.(i),mkpat i,cl.(i))))
and align_tree nal isgoal (e,c as rhs) = match nal with
| [] -> [[],rhs]
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index a5c4ecd3b..8904e2b7b 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -432,7 +432,7 @@ let mis_make_indrec env sigma listdepkind mib =
mis_make_case_com dep env sigma indi (mibi,mipi) kind
in
(* Body of mis_make_indrec *)
- List.tabulate make_one_rec nrec
+ List.init nrec make_one_rec
(**********************************************************************)
(* This builds elimination predicate for Case tactic *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index ef95fbb5c..610bde687 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -92,7 +92,7 @@ let mis_nf_constructor_type (ind,mib,mip) j =
and nconstr = Array.length mip.mind_consnames in
let make_Ik k = mkInd ((fst ind),ntypes-k-1) in
if j > nconstr then error "Not enough constructors in the type.";
- substl (List.tabulate make_Ik ntypes) specif.(j-1)
+ substl (List.init ntypes make_Ik) specif.(j-1)
(* Arity of constructors excluding parameters and local defs *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 732001fde..24ae6c1d0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -293,7 +293,7 @@ let contract_cofix ?env (bodynum,(names,types,bodies as typedbodies)) cst =
match env with
| None -> bd
| Some e -> magicaly_constant_of_fixbody e bd names.(ind) in
- let closure = List.tabulate make_Fi nbodies in
+ let closure = List.init nbodies make_Fi in
substl closure bodies.(bodynum)
let reduce_mind_case mia =
@@ -322,7 +322,7 @@ let contract_fix ?env ((recindices,bodynum),(names,types,bodies as typedbodies))
match env with
| None -> bd
| Some e -> magicaly_constant_of_fixbody e bd names.(ind) in
- let closure = List.tabulate make_Fi nbodies in
+ let closure = List.init nbodies make_Fi in
substl closure bodies.(bodynum)
let fix_recarg ((recindices,bodynum),_) stack =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 508569f0d..b46b69c62 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -457,7 +457,7 @@ let contract_fix_use_function env sigma f
((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
let nbodies = Array.length recindices in
let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
- let lbodies = List.tabulate make_Fi nbodies in
+ let lbodies = List.init nbodies make_Fi in
substl_checking_arity env (List.rev lbodies) (nf_beta sigma bodies.(bodynum))
let reduce_fix_use_function env sigma f whfun fix stack =
@@ -480,7 +480,7 @@ let contract_cofix_use_function env sigma f
(bodynum,(_names,_,bodies as typedbodies)) =
let nbodies = Array.length bodies in
let make_Fi j = (mkCoFix(j,typedbodies), f j) in
- let subbodies = List.tabulate make_Fi nbodies in
+ let subbodies = List.init nbodies make_Fi in
substl_checking_arity env (List.rev subbodies)
(nf_beta sigma bodies.(bodynum))
diff --git a/printing/printer.ml b/printing/printer.ml
index 8fc38bc6c..ac7761994 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -735,7 +735,7 @@ let print_one_inductive env mib ((_,i) as ind) =
brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
let print_mutual_inductive env mind mib =
- let inds = List.tabulate (fun x -> (mind,x)) (Array.length mib.mind_packets)
+ let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
in
hov 0 (
str (if mib.mind_finite then "Inductive " else "CoInductive ") ++
diff --git a/tactics/auto.ml b/tactics/auto.ml
index f9b45bdfb..e05c5384a 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -873,10 +873,9 @@ let interp_hints =
let constr_hints_of_ind qid =
let ind = global_inductive_with_alias qid in
Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
- List.tabulate (fun i -> let c = (ind,i+1) in
+ List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in
let gr = ConstructRef c in
- None, true, PathHints [gr], IsGlobal gr)
- (nconstructors ind) in
+ None, true, PathHints [gr], IsGlobal gr) in
HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
| HintsExtern (pri, patcom, tacexp) ->
let pat = Option.map fp patcom in
@@ -1069,7 +1068,7 @@ let expand_constructor_hints env lems =
List.map_append (fun (sigma,lem) ->
match kind_of_term lem with
| Ind ind ->
- List.tabulate (fun i -> mkConstruct (ind,i+1)) (nconstructors ind)
+ List.init (nconstructors ind) (fun i -> mkConstruct (ind,i+1))
| _ ->
[prepare_hint env (sigma,lem)]) lems
diff --git a/tactics/inv.ml b/tactics/inv.ml
index c99c15a45..7308b7091 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -472,7 +472,7 @@ let raw_inversion inv_kind id status names gl =
(fun id ->
(tclTHEN
(apply_term (mkVar id)
- (List.tabulate (fun _ -> Evarutil.mk_new_meta()) neqns))
+ (List.init neqns (fun _ -> Evarutil.mk_new_meta())))
reflexivity))])
gl
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ac783adf3..210800955 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -938,14 +938,14 @@ let descend_in_conjunctions tac exit c gl =
let elim = pf_apply build_case_analysis_scheme gl ind false sort in
NotADefinedRecordUseScheme elim in
tclFIRST
- (List.tabulate (fun i gl ->
+ (List.init n (fun i gl ->
match make_projection (project gl) params cstr sign elim i n c with
| None -> tclFAIL 0 (mt()) gl
| Some (p,pt) ->
tclTHENS
(internal_cut id pt)
[refine p; (* Might be ill-typed due to forbidden elimination. *)
- tclTHEN (tac (not isrec) (mkVar id)) (thin [id])] gl) n)
+ tclTHEN (tac (not isrec) (mkVar id)) (thin [id])] gl))
gl
| None ->
raise Exit
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index b12378c56..4dd00301f 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -38,7 +38,7 @@ let abstract_inductive hyps nparams inds =
let ntyp = List.length inds in
let nhyp = named_context_length hyps in
let args = instance_from_named_context (List.rev hyps) in
- let subs = List.tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in
+ let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in
let inds' =
List.map
(function (tname,arity,cnames,lc) ->
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 616430007..bed262bbb 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -178,7 +178,7 @@ let beq_scheme_msg mind =
(* TODO: mutual inductive case *)
str "Boolean equality on " ++
pr_enum (fun ind -> quote (Printer.pr_inductive (Global.env()) ind))
- (List.tabulate (fun i -> (mind,i)) (Array.length mib.mind_packets))
+ (List.init (Array.length mib.mind_packets) (fun i -> (mind,i)))
let declare_beq_scheme_with l kn =
try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 6b8780cda..092c329f3 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -31,7 +31,7 @@ let trace s =
let succfix (depth, fixrels) =
(succ depth, List.map succ fixrels)
-let mkMetas n = List.tabulate (fun _ -> Evarutil.mk_new_meta ()) n
+let mkMetas n = List.init n (fun _ -> Evarutil.mk_new_meta ())
let check_evars env evm =
List.iter
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 22:48:07 +0000