Upgrading some local function as a general-purpose combinator Option.List.map.

3 files changed, 20 insertions, 14 deletions

diff --git a/lib/option.ml b/lib/option.ml
index fbb883d30..f3047a3ca 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -188,4 +188,14 @@ module List =
 	 |None -> find f t
 	 |x -> x
 
+  let map f l =
+    let rec aux f l = match l with
+    | [] -> []
+    | x :: l ->
+      match f x with
+      | None -> raise Exit
+      | Some y -> y :: aux f l
+    in
+    try Some (aux f l) with Exit -> None
+
 end
diff --git a/lib/option.mli b/lib/option.mli
index 5e085620e..a336c895c 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -123,4 +123,10 @@ module List : sig
   val flatten : 'a option list -> 'a list
 
   val find : ('a -> 'b option) -> 'a list -> 'b option
+
+  (** [List.map f [a1;...;an]] is the list [Some [b1;...;bn]] if
+      for all i, there is a [bi] such that [f ai] is [Some bi]; it is
+      [None] if, for at least one i, [f ai] is [None]. *)
+  val map : ('a -> 'b option) -> 'a list -> 'b list option
+
 end
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f0d011477..4ada91eb5 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -470,23 +470,13 @@ let free_vars_and_rels_up_alias_expansion sigma aliases c =
 (* Managing pattern-unification *)
 (********************************)
 
-let map_all f l =
-  let rec map_aux f l = match l with
-  | [] -> []
-  | x :: l ->
-    match f x with
-    | None -> raise Exit
-    | Some y -> y :: map_aux f l
-  in
-  try Some (map_aux f l) with Exit -> None
-
 let expand_and_check_vars sigma aliases l =
   let map a = match get_alias_chain_of sigma aliases a with
   | None, [] -> Some a
   | None, a :: _ -> Some a
   | Some _, _ -> None
   in
-  map_all map l
+  Option.List.map map l
 
 let alias_distinct l =
   let rec check (rels, vars) = function
@@ -540,7 +530,7 @@ let is_unification_pattern_meta env evd nb m l t =
   | Rel n -> if n <= nb then Some (RelAlias n) else None
   | _ -> None
   in
-  match map_all map l with
+  match Option.List.map map l with
   | Some l ->
     begin match find_unification_pattern_args env evd l t with
     | Some _ as x when not (dependent evd (mkMeta m) t) -> x
@@ -550,10 +540,10 @@ let is_unification_pattern_meta env evd nb m l t =
     None
 
 let is_unification_pattern_evar env evd (evk,args) l t =
-  match map_all (fun c -> to_alias evd c) l with
+  match Option.List.map (fun c -> to_alias evd c) l with
   | Some l when noccur_evar env evd evk t ->
     let args = remove_instance_local_defs evd evk args in
-    let args = map_all (fun c -> to_alias evd c) args in
+    let args = Option.List.map (fun c -> to_alias evd c) args in
     begin match args with
     | None -> None
     | Some args ->