diff options
| author | aspiwack | 2007-12-14 11:48:05 +0000 |
|---|---|---|
| committer | aspiwack | 2007-12-14 11:48:05 +0000 |
| commit | 7ad1614bc7a21e6630fffb523b56b3f26dddc3a1 (patch) | |
| tree | 4180c100d1c8681082f738e77b84ba6118487afb /lib | |
| parent | 8bddc438fa3a393a799c388843e235e2a63160fb (diff) | |
Petite correction de Option.default (default faisait un Option.map
gratuit, je me suis décidé pour quelque chose de plus atomique).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10379 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/option.ml | 7 | ||||
| -rw-r--r-- | lib/option.mli | 6 |
2 files changed, 6 insertions, 7 deletions
diff --git a/lib/option.ml b/lib/option.ml index 5539058136..95a18396bb 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -100,10 +100,9 @@ let fold_right f x a = (** {6 More Specific operations} ***) -(** [default f x a] is [f y] if [x] is [Some y] and [a] otherwise. *) -let default f x a = - match x with - | Some y -> f y +(** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *) +let default a = function + | Some y -> y | _ -> a (** [lift f x] is the same as [map f x]. *) diff --git a/lib/option.mli b/lib/option.mli index 4047ebe1a2..c1260d9acf 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -69,10 +69,10 @@ val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b (** {6 More Specific Operations} ***) -(** [default f x a] is [f y] if [x] is [Some y] and [a] otherwise. *) -val default : ('a -> 'b) -> 'a option -> 'b -> 'b +(** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *) +val default : 'a -> 'a option -> 'a -(** [lift f x] is the same as [map f x]. *) +(** [lift] is the same as {!map}. *) val lift : ('a -> 'b) -> 'a option -> 'b option (** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and |