Commit intermédiaire express de réparation de coqide.ml, que j'avais

tout cassé hier sans m'en rendre compte (le soucis de travailler sur un 
ordinateur où j'ai pas installé lablgtk2).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10347 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 18 insertions, 8 deletions

diff --git a/lib/option.ml b/lib/option.ml
index 96b9c70e88..0ed36b0026 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -29,6 +29,8 @@ let get = function
   | Some y -> y
   | _ -> raise IsNone
 
+(** [make x] returns [Some x]. *)
+let make x = Some x
 
 (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
 let flatten = function
@@ -72,6 +74,15 @@ let fold_left f a = function
   | Some y -> f a y
   | _ -> a
 
+(** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w].
+    It is [a] if both [x] and [y] are [None]. Otherwise it raises
+    [Heterogeneous]. *)
+let fold_left2 f a x y =
+  match x,y with
+  | Some x, Some y -> f a x y
+  | None, None -> a
+  | _ -> raise Heterogeneous
+
 (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *)
 let fold_right f x a = 
   match x with
diff --git a/lib/option.mli b/lib/option.mli
index 0a22697e75..f98c45ee72 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -25,6 +25,8 @@ exception IsNone
     if [x] equals [None]. *)
 val get : 'a option -> 'a
 
+(** [make x] returns [Some x]. *)
+val make : 'a -> 'a option
 
 (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
 val flatten : 'a option option -> 'a option
@@ -53,6 +55,11 @@ val smartmap : ('a -> 'a) -> 'a option -> 'a option
 (** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *)
 val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b
 
+(** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w].
+    It is [a] if both [x] and [y] are [None]. Otherwise it raises
+    [Heterogeneous]. *)
+val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a
+
 (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *)
 val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
 
diff --git a/lib/util.ml b/lib/util.ml
index 389d0e1296..b61cd88ff6 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -788,15 +788,10 @@ let interval n m =
   in 
   interval_n ([],m)
 
-let in_some x = Some x
-
 let option_cons a l = match a with
   | Some x -> x::l
   | None -> l
 
-let option_fold_left2 f e a b = match (a,b) with
-  | Some x, Some y -> f e x y
-
 let option_compare f a b = match (a,b) with
   | None, None -> true
   | Some a', Some b' -> f a' b'
diff --git a/lib/util.mli b/lib/util.mli
index 0282f45f5b..71262bb4cd 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -223,10 +223,7 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list
 
 val interval : int -> int -> int list
 
-val in_some : 'a -> 'a option
 val option_cons : 'a option -> 'a list -> 'a list
-val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option ->
-  'c option -> 'a
 val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool 
 val filter_some : 'a option list -> 'a list