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

7 files changed, 20 insertions, 13 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index cda306eb29..9860870ca0 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -13,9 +13,6 @@ open Vernacexpr
 open Coq
 open Ideutils
   
-let Option.get s = match s with 
-  | None -> failwith "Internal error in Option.get" | Some f -> f
-      
 let cb_ = ref None
 let cb () = ((Option.get !cb_):GData.clipboard)
 let last_cb_content = ref ""
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index fcf3839377..e29f172109 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -451,7 +451,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
 	 & List.length eqnl1 = List.length eqnl2 ->
       let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in
       let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in
-      let sigma = option_fold_left2 (match_ alp metas) sigma rtno1' rtno2' in
+      let sigma = Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2' in
       let sigma = List.fold_left2 
        (fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in
       List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2
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
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 6a73943b92..29e8012fea 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -381,7 +381,7 @@ let (in_modtype,out_modtype) =
       load_function = load_modtype;
       subst_function = subst_modtype;
       classify_function = classify_modtype;
-      export_function = in_some }
+      export_function = Option.make }