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

1 files changed, 11 insertions, 0 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