Suppression de la dépendance en Map.fold de ocaml dont la sémantique a

changé entre les version 3.08.4 et 3.09.0 (influe notamment sur l'ordre
d'application des Hints de auto)


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

3 files changed, 18 insertions, 12 deletions

diff --git a/lib/gmap.ml b/lib/gmap.ml
index 4febb3ad1d..858cb40c8b 100644
--- a/lib/gmap.ml
+++ b/lib/gmap.ml
@@ -8,7 +8,7 @@
 (* $Id$ *)
 
 (* Maps using the generic comparison function of ocaml. Code borrowed from
-   the ocaml standard library. *)
+   the ocaml standard library (Copyright 1996, INRIA). *)
 
     type ('a,'b) t =
         Empty
@@ -81,12 +81,23 @@
           let c = Pervasives.compare x v in
           c = 0 || mem x (if c < 0 then l else r)
 
-    let rec merge t1 t2 =
+    let rec min_binding = function
+        Empty -> raise Not_found
+      | Node(Empty, x, d, r, _) -> (x, d)
+      | Node(l, x, d, r, _) -> min_binding l
+
+    let rec remove_min_binding = function
+        Empty -> invalid_arg "Map.remove_min_elt"
+      | Node(Empty, x, d, r, _) -> r
+      | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r
+
+    let merge t1 t2 =
       match (t1, t2) with
         (Empty, t) -> t
       | (t, Empty) -> t
-      | (Node(l1, v1, d1, r1, h1), Node(l2, v2, d2, r2, h2)) ->
-          bal l1 v1 d1 (bal (merge r1 l2) v2 d2 r2)
+      | (_, _) ->
+          let (x, d) = min_binding t2 in
+          bal t1 x d (remove_min_binding t2)
 
     let rec remove x = function
         Empty ->
@@ -109,6 +120,9 @@
         Empty               -> Empty
       | Node(l, v, d, r, h) -> Node(map f l, v, f d, map f r, h)
 
+    (* Maintien de fold_right par compatibilité (changé en fold_left dans
+       ocaml-3.09.0) *)
+
     let rec fold f m accu =
       match m with
         Empty -> accu
diff --git a/lib/util.ml b/lib/util.ml
index df5be249d7..4f64b3a6e4 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -119,10 +119,6 @@ module Stringset = Set.Make(struct type t = string let compare = compare end)
 
 module Stringmap = Map.Make(struct type t = string let compare = compare end)
 
-let stringmap_to_list m = Stringmap.fold (fun s y l -> (s,y)::l) m []
-
-let stringmap_dom m = Stringmap.fold (fun s _ l -> s::l) m []
-
 (* Lists *)
 
 let list_add_set x l = if List.mem x l then l else x::l
diff --git a/lib/util.mli b/lib/util.mli
index 3993fc8519..6fbe23c289 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -72,12 +72,8 @@ val string_string_contains : where:string -> what:string -> bool
 val parse_loadpath : string -> string list
 
 module Stringset : Set.S with type elt = string
-
 module Stringmap : Map.S with type key = string
 
-val stringmap_to_list : 'a Stringmap.t -> (string * 'a) list 
-val stringmap_dom : 'a Stringmap.t -> string list
-
 (*s Lists. *)
 
 val list_add_set : 'a -> 'a list -> 'a list