diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-24 16:18:20 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-24 16:18:20 +0000 |
| commit | aa1baddd23bb3a0411995cd2684774b70427fa2f (patch) | |
| tree | 3978455e0c17aca505664c7705a98347200ff17e | |
| parent | 350643b1424b5aead618d93c61c736cba8d9bf92 (diff) | |
Fix the semantic of the new List.remove_assoc_f
Unlike Ocaml's stdlib List.remove_assoc, I was raising Not_found
when the key to remove wasn't there...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16931 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | lib/cList.ml | 3 | ||||
| -rw-r--r-- | lib/cList.mli | 3 |
2 files changed, 5 insertions, 1 deletions
diff --git a/lib/cList.ml b/lib/cList.ml index 6559efd40..140728242 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -736,7 +736,8 @@ let rec assoc_f f a = function | (x, e) :: xs -> if f a x then e else assoc_f f a xs | [] -> raise Not_found -let remove_assoc_f f a l = remove_first (fun (x,_) -> f a x) l +let remove_assoc_f f a l = + try remove_first (fun (x,_) -> f a x) l with Not_found -> l let mem_assoc_f f a l = List.exists (fun (x,_) -> f a x) l diff --git a/lib/cList.mli b/lib/cList.mli index 3968a4adf..6b9f2a8c2 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -160,7 +160,10 @@ sig val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool val except : 'a eq -> 'a -> 'a list -> 'a list val remove : 'a eq -> 'a -> 'a list -> 'a list + val remove_first : ('a -> bool) -> 'a list -> 'a list + (** Remove the first element satisfying a predicate, or raise [Not_found] *) + val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool val sep_last : 'a list -> 'a * 'a list |