aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/wg_Command.ml2
-rw-r--r--ide/wg_Notebook.ml2
-rw-r--r--interp/notation_ops.ml2
-rw-r--r--interp/reserve.ml2
-rw-r--r--lib/cList.ml73
-rw-r--r--lib/cList.mli95
-rw-r--r--lib/util.ml9
-rw-r--r--library/declare.ml2
-rw-r--r--plugins/extraction/extract_env.ml2
-rw-r--r--plugins/extraction/mlutil.ml4
-rw-r--r--plugins/extraction/table.ml2
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/invfun.ml3
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/evarutil.ml4
-rw-r--r--pretyping/evd.ml10
-rw-r--r--pretyping/recordops.ml4
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--tactics/equality.ml9
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--toplevel/command.ml6
21 files changed, 126 insertions, 113 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 5a72669b8..2e4ce364d 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -55,7 +55,7 @@ class command_window coqtop =
let remove_cb () =
let index = notebook#current_page in
let () = notebook#remove_page index in
- views := Util.List.filter_i (fun i x -> i <> index) !views
+ views := Util.List.filteri (fun i x -> i <> index) !views
in
let _ =
toolbar#insert_button
diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml
index c75b371fe..7a4ddc010 100644
--- a/ide/wg_Notebook.ml
+++ b/ide/wg_Notebook.ml
@@ -51,7 +51,7 @@ object(self)
method pages = term_list
method remove_page index =
- term_list <- Util.List.filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list;
+ term_list <- Util.List.filteri (fun i x -> if i = index then kill_page x; i <> index) term_list;
super#remove_page index
method current_term =
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 3429ab7b9..c5cc1438b 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -710,7 +710,7 @@ and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
match_in u alp metas sigma rhs1 rhs2
let match_notation_constr u c (metas,pat) =
- let vars = List.split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in
+ let vars = List.partition (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in
let vars = (List.map fst (fst vars), List.map fst (snd vars)) in
let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in
(* Reorder canonically the substitution *)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 7a2d4bfe7..914a85fe8 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -79,7 +79,7 @@ let revert_reserved_type t =
let t = Detyping.detype false [] [] t in
List.try_find
(fun (pat,id) ->
- try let _ = Notation_ops.match_notation_constr false t ([],pat) in Name id
+ try let _ = Notation_ops.match_notation_constr false t ([], pat) in Name id
with Notation_ops.No_match -> failwith "") l
with Not_found | Failure _ -> Anonymous
diff --git a/lib/cList.ml b/lib/cList.ml
index bc2109167..c5845e74c 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -87,8 +87,7 @@ sig
('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
val map4 :
('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
- val map_to_array : ('a -> 'b) -> 'a list -> 'b array
- val filter_i :
+ val filteri :
(int -> 'a -> bool) -> 'a list -> 'a list
(** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
@@ -105,8 +104,7 @@ sig
(** [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 iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
- val iter_i : (int -> 'a -> unit) -> 'a list -> unit
+ val iteri : (int -> 'a -> unit) -> 'a list -> unit
val fold_right_i : (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
val fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
val fold_right_and_left :
@@ -130,9 +128,7 @@ sig
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 split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
- val partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
val firstn : int -> 'a list -> 'a list
val last : 'a list -> 'a
val lastn : int -> 'a list -> 'a list
@@ -366,28 +362,34 @@ let subtractq l1 l2 =
if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1
let tabulate f len =
- let rec tabrec n =
- if n = len then [] else (f n)::(tabrec (n+1))
+ let rec loop p i =
+ if len <= i then ()
+ else
+ let c = { head = f i; tail = [] } in
+ let () = p.tail <- cast c in
+ loop c (succ i)
in
- tabrec 0
+ let dummy = { head = Obj.magic 0; tail = [] } in
+ loop dummy 0;
+ dummy.tail
let addn n v =
let rec aux n l =
if n = 0 then l
- else aux (pred n) (v::l)
+ else aux (pred n) (v :: l)
in
- if n < 0 then invalid_arg "List.addn"
- else aux n
+ if n < 0 then invalid_arg "List.addn"
+ else aux n
let make n v = addn n v []
let assign l n e =
- let rec assrec stk = function
- | ((h::t), 0) -> List.rev_append stk (e::t)
- | ((h::t), n) -> assrec (h::stk) (t, n-1)
+ let rec assrec stk l i = match l, i with
+ | ((h::t), 0) -> List.rev_append stk (e :: t)
+ | ((h::t), n) -> assrec (h :: stk) t (pred n)
| ([], _) -> failwith "List.assign"
in
- assrec [] (l,n)
+ assrec [] l n
let rec smartmap f l = match l with
[] -> l
@@ -396,12 +398,7 @@ let rec smartmap f l = match l with
if h'==h && tl'==tl then l
else h'::tl'
-let map_left f = (* ensures the order in case of side-effects *)
- let rec map_rec = function
- | [] -> []
- | x::l -> let v = f x in v :: map_rec l
- in
- map_rec
+let map_left = map
let map2_i f i l1 l2 =
let rec map_i i = function
@@ -427,9 +424,6 @@ let map4 f l1 l2 l3 l4 =
in
map (l1,l2,l3,l4)
-let map_to_array f l =
- Array.of_list (List.map f l)
-
let rec smartfilter f l = match l with
[] -> l
| h::tl ->
@@ -505,15 +499,7 @@ let fold_right_and_left f l hd =
| a::l -> let hd = aux (a::tl) l in f hd a tl
in aux [] l
-let iter3 f l1 l2 l3 =
- let rec iter = function
- | ([], [], []) -> ()
- | ((h1::t1), (h2::t2), (h3::t3)) -> f h1 h2 h3; iter (t1,t2,t3)
- | (_, _, _) -> invalid_arg "map3"
- in
- iter (l1,l2,l3)
-
-let iter_i f l = fold_left_i (fun i _ x -> f i x) 0 () l
+let iteri f l = fold_left_i (fun i _ x -> f i x) 0 () l
let for_all_i p =
let rec for_all_p i = function
@@ -539,7 +525,7 @@ let rec assoc_snd_in_triple x = function
[] -> raise Not_found
| (a,b,_)::l -> if Pervasives.compare a x = 0 then b else assoc_snd_in_triple x l
-let add_set x l = if List.mem x l then l else x::l
+let add_set x l = if List.mem x l then l else x :: l
let eq_set l1 l2 =
let rec aux l1 = function
@@ -550,7 +536,7 @@ let eq_set l1 l2 =
let for_all2eq f l1 l2 =
try List.for_all2 f l1 l2 with Invalid_argument _ -> false
-let filter_i p =
+let filteri p =
let rec filter_i_rec i = function
| [] -> []
| x::l -> let l' = filter_i_rec (succ i) l in if p i x then x::l' else l'
@@ -677,16 +663,6 @@ let split_when p =
in
split_when_loop []
-(* [split_by p l] splits [l] into two lists [(l1,l2)] such that elements of
- [l1] satisfy [p] and elements of [l2] do not; order is preserved *)
-let split_by p =
- let rec split_by_loop = function
- | [] -> ([],[])
- | a::l ->
- let (l1,l2) = split_by_loop l in if p a then (a::l1,l2) else (l1,a::l2)
- in
- split_by_loop
-
let rec split3 = function
| [] -> ([], [], [])
| (x,y,z)::l ->
@@ -697,9 +673,6 @@ let rec insert_in_class f a = function
| (b::_ as l)::classes when f a b -> (a::l)::classes
| l::classes -> l :: insert_in_class f a classes
-let partition_by f l =
- List.fold_right (insert_in_class f) l []
-
let firstn n l =
let rec aux acc = function
| (0, l) -> List.rev acc
@@ -840,7 +813,7 @@ let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> h
(* Factorize lists of pairs according to the left argument *)
let rec factorize_left = function
| (a,b)::l ->
- let al,l' = split_by (fun (a',b) -> a=a') l in
+ let al,l' = partition (fun (a',b) -> a=a') l in
(a,(b::List.map snd al)) :: factorize_left l'
| [] ->
[]
diff --git a/lib/cList.mli b/lib/cList.mli
index c530a2081..87eb3aee7 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -8,6 +8,7 @@
(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *)
+(** Module type [S] is the one from OCaml Stdlib. *)
module type S =
sig
val length : 'a list -> int
@@ -57,58 +58,85 @@ module type ExtS =
sig
include S
val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
+ (** Lexicographic order on lists. *)
+
val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
+ (** Lifts equality to list type. *)
+
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. *)
+
val eq_set : 'a list -> 'a list -> bool
+ (** Test equality up to permutation. *)
+
val intersect : 'a list -> 'a list -> 'a list
val union : 'a list -> 'a list -> 'a list
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
+ (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *)
+
val make : int -> 'a -> 'a list
+ (** [make n x] returns a list made of [n] times [x]. Raise
+ [Invalid_argument "List.make"] if [n] is negative. *)
+
val assign : 'a list -> int -> 'a -> 'a list
+ (** [assign l i x] set the [i]-th element of [l] to [x], starting from [0]. *)
+
val distinct : 'a list -> bool
+ (** Return [true] if all elements of the list are distinct. *)
+
val duplicates : 'a list -> 'a list
+ (** Return the list of unique elements which appear at least twice. Elements
+ are kept in the order of their first appearance. *)
+
val filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
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
val filter_along : ('a -> bool) -> 'a list -> 'b list -> 'b 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
+ (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i
+ [f ai == ai], then [smartmap f l == l] *)
+
val map_left : ('a -> 'b) -> 'a list -> 'b list
+ (** As [map] but ensures the left-to-right order of evaluation. *)
+
val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
+ (** As [map] but with the index, which starts from [0]. *)
+
val map2_i :
(int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
val map3 :
('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
- val map4 :
- ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
- val map_to_array : ('a -> 'b) -> 'a list -> 'b array
- val filter_i :
- (int -> 'a -> bool) -> 'a list -> 'a list
+ val map4 : ('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
+ (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
+ [f ai = true], then [smartfilter f l == l] *)
- (** [index] returns the 1st index of an element in a list (counting from 1) *)
val index : 'a -> 'a list -> int
+ (** [index] returns the 1st index of an element in a list (counting from 1). *)
+
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
+ (** [unique_index x l] returns [Not_found] if [x] doesn't occur exactly once. *)
- (** [index0] behaves as [index] except that it starts counting at 0 *)
val index0 : 'a -> 'a list -> int
+ (** [index0] behaves as [index] except that it starts counting at 0. *)
+
val index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
- val iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
- val iter_i : (int -> 'a -> unit) -> 'a list -> unit
+
+ val iteri : (int -> 'a -> unit) -> 'a list -> unit
+ (** As [iter] but with the index argument (starting from 0). *)
+
val fold_right_i : (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
val fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
val fold_right_and_left :
@@ -124,60 +152,73 @@ sig
val sep_last : 'a list -> 'a * 'a list
val try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
val try_find : ('a -> 'b) -> 'a list -> 'b
+
val uniquize : 'a list -> 'a list
+ (** Return the list of elements without duplicates. *)
- (** merges two sorted lists and preserves the uniqueness property: *)
val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
+ (** Merge two sorted lists and preserves the uniqueness property. *)
+
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 split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
- val partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
val firstn : int -> 'a list -> 'a list
val last : 'a list -> 'a
val lastn : int -> 'a list -> 'a list
val skipn : int -> 'a list -> 'a list
val skipn_at_least : int -> 'a list -> 'a list
+
val addn : int -> 'a -> 'a list -> 'a list
+ (** [addn n x l] adds [n] times [x] on the left of [l]. *)
+
val prefix_of : 'a list -> 'a list -> bool
+ (** [prefix_of l1 l2] returns [true] if [l1] is a prefix of [l2], [false]
+ otherwise. *)
- (** [drop_prefix p l] returns [t] if [l=p++t] else return [l] *)
val drop_prefix : 'a list -> 'a list -> 'a list
+ (** [drop_prefix p l] returns [t] if [l=p++t] else return [l]. *)
+
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
+ (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)]. *)
+
val join_map : ('a -> 'b list) -> 'a list -> 'b list
+ (** Alias of [map_append]. *)
- (** 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
+ (** As [map_append]. Raises [Invalid_argument _] if the two lists don't have
+ the same length. *)
+
val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
+ val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c 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
+ val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
(** 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
+ val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b 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
+ (** combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
+
val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
- (** Keep only those products that do not return None *)
val cartesian_filter :
('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
+ (** Keep only those products that do not return None *)
+
val cartesians_filter :
('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
diff --git a/lib/util.ml b/lib/util.ml
index 42ad11ee1..102541731 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -442,12 +442,9 @@ let interval n m =
interval_n ([],m)
-let map_succeed f =
- let rec map_f = function
- | [] -> []
- | h::t -> try (let x = f h in x :: map_f t) with Failure _ -> map_f t
- in
- map_f
+let map_succeed f l =
+ let filter x = try Some (f x) with Failure _ -> None in
+ List.map_filter filter l
(*s Memoization *)
diff --git a/library/declare.ml b/library/declare.ml
index 63a2c03a7..aa10cf314 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -183,7 +183,7 @@ let declare_constant ?(internal = UserVerbose) id (cd,kind) =
(** Declaration of inductive blocks *)
let declare_inductive_argument_scopes kn mie =
- List.iter_i (fun i {mind_entry_consnames=lc} ->
+ List.iteri (fun i {mind_entry_consnames=lc} ->
Notation.declare_ref_arguments_scope (IndRef (kn,i));
for j=1 to List.length lc do
Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j));
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index aaf6f2bd0..9fe5606b9 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -152,7 +152,7 @@ let factor_fix env l cb msb =
if List.length msb < n-1 then raise Impossible;
let msb', msb'' = List.chop (n-1) msb in
let labels = Array.make n l in
- List.iter_i
+ List.iteri
(fun j ->
function
| (l,SFBconst cb') ->
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 01b98b131..e3abab82b 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -969,7 +969,7 @@ and simpl_case o typ br e =
else ([], Pwild, ast_pop f)
in
let brl = Array.to_list br in
- let brl_opt = List.filter_i (fun i _ -> not (Intset.mem i ints)) brl in
+ let brl_opt = List.filteri (fun i _ -> not (Intset.mem i ints)) brl in
let brl_opt = brl_opt @ [last_br] in
MLcase (typ, e, Array.of_list brl_opt)
| None -> MLcase (typ, e, br)
@@ -1164,7 +1164,7 @@ let general_optimize_fix f ids n args m c =
| MLrel j when v.(j-1)>=0 ->
if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
| _ -> raise Impossible
- in List.iter_i aux args;
+ in List.iteri aux args;
let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
let new_f = anonym_tmp_lams (MLapp (MLrel (n+m+1),args_f)) m in
let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 6151abf6e..4322ac95f 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -877,7 +877,7 @@ let extract_inductive r s l optstr =
Lib.add_anonymous_leaf (in_customs (g,[],s));
Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s)))
optstr;
- List.iter_i
+ List.iteri
(fun j s ->
let g = ConstructRef (ip,succ j) in
Lib.add_anonymous_leaf (inline_extraction (true,[g]));
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 490d52555..b820489f5 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1238,7 +1238,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b
let l = ref [] in
let _ =
try
- List.iter_i
+ List.iteri
(fun i ((n,nt,is_defined) as param) ->
if Array.for_all
(fun l ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d8255e834..bbc9ff93b 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -122,10 +122,11 @@ let generate_type g_to_f f graph i =
| _ -> let j = !i in incr i;mkRel (nb_args - j + 1)
in
(*i We need to name the vars [res] and [fv] i*)
+ let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in
let res_id =
Namegen.next_ident_away_in_goal
(id_of_string "res")
- (map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "") fun_ctxt)
+ (List.map_filter filter fun_ctxt)
in
let fv_id =
Namegen.next_ident_away_in_goal
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0ece3496e..98cc42aaf 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -912,7 +912,7 @@ let adjust_impossible_cases pb pred tomatch submat =
(* we add an "assert false" case *)
let pats = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) tomatch in
let aliasnames =
- map_succeed (function Alias _ | NonDepAlias -> Anonymous | _ -> failwith"") tomatch
+ List.map_filter (function Alias _ | NonDepAlias -> Some Anonymous | _ -> None) tomatch
in
[ { patterns = pats;
rhs = { rhs_env = pb.env;
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 700b168ae..af3227729 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1120,7 +1120,7 @@ let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_e
res
let effective_projections =
- map_succeed (function Invertible c -> c | _ -> failwith"")
+ List.map_filter (function Invertible c -> Some c | _ -> None)
let instance_of_projection f env t evd projs =
let ty = lazy (nf_evar evd (Retyping.get_type_of env evd t)) in
@@ -1407,7 +1407,7 @@ let solve_evar_evar ?(force=false) f g env evd (evk1,args1 as ev1) (evk2,args2 a
if are_canonical_instances args1 args2 env then
(* If instances are canonical, we solve the problem in linear time *)
let sign = evar_filtered_context (Evd.find evd evk2) in
- let id_inst = List.map_to_array (fun (id,_,_) -> mkVar id) sign in
+ let id_inst = Array.map (fun (id,_,_) -> mkVar id) (Array.of_list sign) in
Evd.define evk2 (mkEvar(evk1,id_inst)) evd
else
let evd,ev1,ev2 =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 7d95e743d..1394f3ba8 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -563,10 +563,12 @@ let meta_list evd = metamap_to_list evd.metas
let find_meta evd mv = Metamap.find mv evd.metas
let undefined_metas evd =
- List.sort Pervasives.compare (map_succeed (function
- | (n,Clval(_,_,typ)) -> failwith ""
- | (n,Cltyp (_,typ)) -> n)
- (meta_list evd))
+ let filter = function
+ | (n,Clval(_,_,typ)) -> None
+ | (n,Cltyp (_,typ)) -> Some n
+ in
+ let m = List.map_filter filter (meta_list evd) in
+ List.sort Pervasives.compare m
let metas_of evd =
List.map (function
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 96b57ae18..f32eb0879 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -199,8 +199,8 @@ let canonical_projections () =
!object_table []
let keep_true_projections projs kinds =
- map_succeed (function (p,(_,true)) -> p | _ -> failwith "")
- (List.combine projs kinds)
+ let filter (p, (_, b)) = if b then Some p else None in
+ List.map_filter filter (List.combine projs kinds)
let cs_pattern_of_constr t =
match kind_of_term t with
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2a6dc35d1..3563e9ca2 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -188,7 +188,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
let reversible_rels = List.map fst li in
if not (List.distinct reversible_rels) then
raise Elimconst;
- List.iter_i (fun i t_i ->
+ List.iteri (fun i t_i ->
if not (List.mem_assoc (i+1) li) then
let fvs = List.map ((+) (i+1)) (Intset.elements (free_rels t_i)) in
if List.intersect fvs reversible_rels <> [] then raise Elimconst)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4d67fef00..7f2ee2e87 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1410,17 +1410,16 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) gl =
(* The set of hypotheses using x *)
let depdecls =
let test (id,_,c as dcl) =
- if id <> hyp && occur_var_in_decl (pf_env gl) x dcl then dcl
- else failwith "caught" in
- List.rev (map_succeed test (pf_hyps gl)) in
+ if id <> hyp && occur_var_in_decl (pf_env gl) x dcl then Some dcl
+ else None in
+ List.rev (List.map_filter test (pf_hyps gl)) in
let dephyps = List.map (fun (id,_,_) -> id) depdecls in
(* Decides if x appears in conclusion *)
let depconcl = occur_var (pf_env gl) x (pf_concl gl) in
(* The set of non-defined hypothesis: they must be abstracted,
rewritten and reintroduced *)
let abshyps =
- map_succeed
- (fun (id,v,_) -> if v=None then mkVar id else failwith "caught")
+ List.map_filter (function (id, None, _) -> Some (mkVar id) | _ -> None)
depdecls in
(* a tactic that either introduce an abstracted and rewritten hyp,
or introduce a definition where x was replaced *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 4ce382df2..057a268f5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1242,7 +1242,7 @@ let rec extract_ids ids = function
let default_fresh_id = id_of_string "H"
let interp_fresh_id ist env l =
- let ids = map_succeed (function ArgVar(_,id) -> id | _ -> failwith "") l in
+ let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in
let avoid = (extract_ids ids ist.lfun) @ ist.avoid_ids in
let id =
if l = [] then default_fresh_id
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c54dc8120..044502cda 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -368,11 +368,11 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
let (_,kn) = declare_mind isrecord mie in
let mind = Global.mind_of_delta_kn kn in
- List.iter_i (fun i (indimpls, constrimpls) ->
+ List.iteri (fun i (indimpls, constrimpls) ->
let ind = (mind,i) in
Autoinstance.search_declaration (IndRef ind);
maybe_declare_manual_implicits false (IndRef ind) indimpls;
- List.iter_i
+ List.iteri
(fun j impls ->
(* Autoinstance.search_declaration (ConstructRef (ind,j));*)
maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls)
@@ -920,7 +920,7 @@ let do_program_recursive fixkind fixl ntns =
in
let indexes =
Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in
- List.iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl
+ List.iteri (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl
end;
Obligations.add_mutual_definitions defs ntns fixkind
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 23:56:50 +0000