--- frama-c-Oxygen-20120901.orig/src/type/datatype.ml	2012-09-19 13:55:23.000000000 +0200
+++ frama-c-Oxygen-20120901/src/type/datatype.ml	2013-02-19 16:36:36.000000000 +0100
@@ -285,8 +285,37 @@
 
 end
 
+module type Set_S = sig
+    type elt
+    type t
+    val empty: t
+    val is_empty: t -> bool
+    val mem: elt -> t -> bool
+    val add: elt -> t -> t
+    val singleton: elt -> t
+    val remove: elt -> t -> t
+    val union: t -> t -> t
+    val inter: t -> t -> t
+    val diff: t -> t -> t
+    val compare: t -> t -> int
+    val equal: t -> t -> bool
+    val subset: t -> t -> bool
+    val iter: (elt -> unit) -> t -> unit
+    val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
+    val for_all: (elt -> bool) -> t -> bool
+    val exists: (elt -> bool) -> t -> bool
+    val filter: (elt -> bool) -> t -> t
+    val partition: (elt -> bool) -> t -> t * t
+    val cardinal: t -> int
+    val elements: t -> elt list
+    val min_elt: t -> elt
+    val max_elt: t -> elt
+    val choose: t -> elt
+    val split: elt -> t -> t * bool * t
+end
+
 module type Set = sig
-  include Set.S
+  include Set_S
   val ty: t Type.t
   val name: string
   val descr: t Descr.t
@@ -1093,7 +1122,7 @@
 module Initial_caml_set = Set
 
 (* ocaml functors are generative *)
-module Set(S: Set.S)(E: S with type t = S.elt)(Info: Functor_info) = struct
+module Set(S: Set_S)(E: S with type t = S.elt)(Info: Functor_info) = struct
 
   let () = check E.equal "equal" E.name Info.module_name
   let () = check E.compare "compare" E.name Info.module_name
--- frama-c-Oxygen-20120901.orig/src/type/datatype.mli	2012-09-19 13:55:23.000000000 +0200
+++ frama-c-Oxygen-20120901/src/type/datatype.mli	2013-02-19 16:36:29.000000000 +0100
@@ -230,9 +230,38 @@
     defining by applying the functor. *)
 end
 
+module type Set_S = sig
+    type elt
+    type t
+    val empty: t
+    val is_empty: t -> bool
+    val mem: elt -> t -> bool
+    val add: elt -> t -> t
+    val singleton: elt -> t
+    val remove: elt -> t -> t
+    val union: t -> t -> t
+    val inter: t -> t -> t
+    val diff: t -> t -> t
+    val compare: t -> t -> int
+    val equal: t -> t -> bool
+    val subset: t -> t -> bool
+    val iter: (elt -> unit) -> t -> unit
+    val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
+    val for_all: (elt -> bool) -> t -> bool
+    val exists: (elt -> bool) -> t -> bool
+    val filter: (elt -> bool) -> t -> t
+    val partition: (elt -> bool) -> t -> t * t
+    val cardinal: t -> int
+    val elements: t -> elt list
+    val min_elt: t -> elt
+    val max_elt: t -> elt
+    val choose: t -> elt
+    val split: elt -> t -> t * bool * t
+end
+
 (** A standard OCaml set signature extended with datatype operations. *)
 module type Set = sig
-  include Set.S
+  include Set_S
   val ty: t Type.t
   val name: string
   val descr: t Descr.t
@@ -602,7 +631,7 @@
   'e Type.t ->
   ('a -> 'b -> 'c -> 'd -> 'e) Type.t
 
-module Set(S: Set.S)(E: S with type t = S.elt)(Info : Functor_info):
+module Set(S: Set_S)(E: S with type t = S.elt)(Info : Functor_info):
   Set with type t = S.t and type elt = E.t
 
 module Map
--- frama-c-Oxygen-20120901.orig/src/wp/qed/src/idxset.ml	2012-09-19 13:55:28.000000000 +0200
+++ frama-c-Oxygen-20120901/src/wp/qed/src/idxset.ml	2013-02-19 16:45:08.000000000 +0100
@@ -20,9 +20,38 @@
 (*                                                                        *)
 (**************************************************************************)
 
+module type Set_S = sig
+    type elt
+    type t
+    val empty: t
+    val is_empty: t -> bool
+    val mem: elt -> t -> bool
+    val add: elt -> t -> t
+    val singleton: elt -> t
+    val remove: elt -> t -> t
+    val union: t -> t -> t
+    val inter: t -> t -> t
+    val diff: t -> t -> t
+    val compare: t -> t -> int
+    val equal: t -> t -> bool
+    val subset: t -> t -> bool
+    val iter: (elt -> unit) -> t -> unit
+    val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
+    val for_all: (elt -> bool) -> t -> bool
+    val exists: (elt -> bool) -> t -> bool
+    val filter: (elt -> bool) -> t -> t
+    val partition: (elt -> bool) -> t -> t * t
+    val cardinal: t -> int
+    val elements: t -> elt list
+    val min_elt: t -> elt
+    val max_elt: t -> elt
+    val choose: t -> elt
+    val split: elt -> t -> t * bool * t
+end
+
 module type S =
 sig
-  include Set.S
+  include Set_S
   val map : (elt -> elt) -> t -> t
   val intersect : t -> t -> bool
 end
--- frama-c-Oxygen-20120901.orig/src/wp/qed/src/idxset.mli	2012-09-19 13:55:28.000000000 +0200
+++ frama-c-Oxygen-20120901/src/wp/qed/src/idxset.mli	2013-02-19 16:45:19.000000000 +0100
@@ -22,9 +22,38 @@
 
 (** Set of indexed elements implemented as Patricia sets. *)
 
+module type Set_S = sig
+    type elt
+    type t
+    val empty: t
+    val is_empty: t -> bool
+    val mem: elt -> t -> bool
+    val add: elt -> t -> t
+    val singleton: elt -> t
+    val remove: elt -> t -> t
+    val union: t -> t -> t
+    val inter: t -> t -> t
+    val diff: t -> t -> t
+    val compare: t -> t -> int
+    val equal: t -> t -> bool
+    val subset: t -> t -> bool
+    val iter: (elt -> unit) -> t -> unit
+    val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
+    val for_all: (elt -> bool) -> t -> bool
+    val exists: (elt -> bool) -> t -> bool
+    val filter: (elt -> bool) -> t -> t
+    val partition: (elt -> bool) -> t -> t * t
+    val cardinal: t -> int
+    val elements: t -> elt list
+    val min_elt: t -> elt
+    val max_elt: t -> elt
+    val choose: t -> elt
+    val split: elt -> t -> t * bool * t
+end
+
 module type S =
 sig
-  include Set.S
+  include Set_S
   val map : (elt -> elt) -> t -> t
   val intersect : t -> t -> bool
 end