simplify (yet again) the extended Set/Map/Hashtbl APIs

the Set signature is moved to a separate Extset module,
instead of being included into Extmap.S. The module hierarchy
becomes simpler, we don't shadow  OCaml standard modules anymore,
and the bug #15270 is fixed, too.

Makefile.in

@@ -104,7 +104,7 @@ LIBGENERATED = src/util/config.ml src/util/rc.ml src/parser/lexer.ml \
 	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
 	       src/driver/driver_lexer.ml src/session/xml.ml
 
-LIB_UTIL = config util opt lists strings extmap exthtbl weakhtbl \
+LIB_UTIL = config util opt lists strings extmap extset exthtbl weakhtbl \
 	   hashcons stdlib exn_printer pp debug loc print_tree \
 	   cmdline warning sysutil rc plugin number
 
@@ -1226,7 +1226,9 @@ endif
 .PHONY: apidoc
 
 MODULESTODOC = \
-	util/exthtbl util/extmap util/rc util/stdlib util/util util/weakhtbl \
+	util/util util/opt util/lists util/strings \
+	util/extmap util/extset util/exthtbl \
+	util/weakhtbl util/stdlib util/rc util/debug \
 	core/ident core/ty core/term core/decl core/theory \
 	core/env core/task \
 	driver/whyconf driver/driver \

src/core/decl.mli

@@ -59,9 +59,9 @@ type prsymbol = private {
   pr_name : ident;
 }
 
-module Mpr : Map.S with type key = prsymbol
-module Spr : Mpr.Set
-module Hpr : XHashtbl.S with type key = prsymbol
+module Mpr : Extmap.S with type key = prsymbol
+module Spr : Extset.S with module M = Mpr
+module Hpr : Exthtbl.S with type key = prsymbol
 module Wpr : Weakhtbl.S with type key = prsymbol
 
 val create_prsymbol : preid -> prsymbol
@@ -103,10 +103,10 @@ and decl_node =
   | Dind   of ind_list          (* (co)inductive predicates *)
   | Dprop  of prop_decl         (* axiom / lemma / goal *)
 
-module Mdecl : Map.S with type key = decl
-module Sdecl : Mdecl.Set
+module Mdecl : Extmap.S with type key = decl
+module Sdecl : Extset.S with module M = Mdecl
 module Wdecl : Weakhtbl.S with type key = decl
-module Hdecl : XHashtbl.S with type key = decl
+module Hdecl : Exthtbl.S with type key = decl
 
 val d_equal : decl -> decl -> bool
 val d_hash : decl -> int

src/core/ident.mli

@@ -20,8 +20,8 @@ type label = private {
   lab_tag    : int;
 }
 
-module Mlab : Map.S with type key = label
-module Slab : Mlab.Set
+module Mlab : Extmap.S with type key = label
+module Slab : Extset.S with module M = Mlab
 
 val lab_equal : label -> label -> bool
 val lab_hash  : label -> int
@@ -37,9 +37,9 @@ type ident = private {
   id_tag    : Weakhtbl.tag;         (* unique magical tag *)
 }
 
-module Mid : Map.S with type key = ident
-module Sid : Mid.Set
-module Hid : XHashtbl.S with type key = ident
+module Mid : Extmap.S with type key = ident
+module Sid : Extset.S with module M = Mid
+module Hid : Exthtbl.S with type key = ident
 module Wid : Weakhtbl.S with type key = ident
 
 val id_equal : ident -> ident -> bool

src/core/term.ml

@@ -1284,7 +1284,7 @@ let rec t_hash_alpha c m t =
 
 let t_hash_alpha = t_hash_alpha (ref (-1)) Mvs.empty
 
-module Hterm_alpha = XHashtbl.Make (struct
+module Hterm_alpha = Exthtbl.Make (struct
   type t = term
   let equal = t_equal_alpha
   let hash = t_hash_alpha

src/core/term.mli

@@ -22,9 +22,9 @@ type vsymbol = private {
   vs_ty   : ty;
 }
 
-module Mvs : Map.S with type key = vsymbol
-module Svs : Mvs.Set
-module Hvs : XHashtbl.S with type key = vsymbol
+module Mvs : Extmap.S with type key = vsymbol
+module Svs : Extset.S with module M = Mvs
+module Hvs : Exthtbl.S with type key = vsymbol
 module Wvs : Weakhtbl.S with type key = vsymbol
 
 val vs_equal : vsymbol -> vsymbol -> bool
@@ -40,9 +40,9 @@ type lsymbol = private {
   ls_value  : ty option;
 }
 
-module Mls : Map.S with type key = lsymbol
-module Sls : Mls.Set
-module Hls : XHashtbl.S with type key = lsymbol
+module Mls : Extmap.S with type key = lsymbol
+module Sls : Extset.S with module M = Mls
+module Hls : Exthtbl.S with type key = lsymbol
 module Wls : Weakhtbl.S with type key = lsymbol
 
 val ls_equal : lsymbol -> lsymbol -> bool
@@ -138,9 +138,9 @@ and term_quant
 
 and trigger = term list list
 
-module Mterm : Map.S with type key = term
-module Sterm : Mterm.Set
-module Hterm : XHashtbl.S with type key = term
+module Mterm : Extmap.S with type key = term
+module Sterm : Extset.S with module M = Mterm
+module Hterm : Exthtbl.S with type key = term
 
 val t_equal : term -> term -> bool
 val t_hash : term -> int
@@ -409,7 +409,7 @@ val t_app_fold :
 
 val t_equal_alpha : term -> term -> bool
 
-module Hterm_alpha : XHashtbl.S with type key = term
+module Hterm_alpha : Exthtbl.S with type key = term
 
 (** Subterm occurrence check and replacement *)
 

src/core/theory.mli

@@ -58,9 +58,9 @@ type meta = private {
 
 val print_meta_desc : Pp.formatter -> meta -> unit
 
-module Mmeta : Map.S with type key = meta
-module Smeta : Mmeta.Set
-module Hmeta : XHashtbl.S with type key = meta
+module Mmeta : Extmap.S with type key = meta
+module Smeta : Extset.S with module M = Mmeta
+module Hmeta : Exthtbl.S with type key = meta
 
 val meta_equal : meta -> meta -> bool
 val meta_hash : meta -> int
@@ -105,9 +105,9 @@ and symbol_map = private {
   sm_pr : prsymbol Mpr.t;
 }
 
-module Mtdecl : Map.S with type key = tdecl
-module Stdecl : Mtdecl.Set
-module Htdecl : XHashtbl.S with type key = tdecl
+module Mtdecl : Extmap.S with type key = tdecl
+module Stdecl : Extset.S with module M = Mtdecl
+module Htdecl : Exthtbl.S with type key = tdecl
 
 val td_equal : tdecl -> tdecl -> bool
 val td_hash : tdecl -> int

src/core/ty.mli

@@ -18,9 +18,9 @@ type tvsymbol = private {
   tv_name : ident;
 }
 
-module Mtv : Map.S with type key = tvsymbol
-module Stv : Mtv.Set
-module Htv : XHashtbl.S with type key = tvsymbol
+module Mtv : Extmap.S with type key = tvsymbol
+module Stv : Extset.S with module M = Mtv
+module Htv : Exthtbl.S with type key = tvsymbol
 
 val tv_equal : tvsymbol -> tvsymbol -> bool
 
@@ -45,14 +45,14 @@ and ty_node = private
   | Tyvar of tvsymbol
   | Tyapp of tysymbol * ty list
 
-module Mts : Map.S with type key = tysymbol
-module Sts : Mts.Set
-module Hts : XHashtbl.S with type key = tysymbol
+module Mts : Extmap.S with type key = tysymbol
+module Sts : Extset.S with module M = Mts
+module Hts : Exthtbl.S with type key = tysymbol
 module Wts : Weakhtbl.S with type key = tysymbol
 
-module Mty : Map.S with type key = ty
-module Sty : Mty.Set
-module Hty : XHashtbl.S with type key = ty
+module Mty : Extmap.S with type key = ty
+module Sty : Extset.S with module M = Mty
+module Hty : Exthtbl.S with type key = ty
 module Wty : Weakhtbl.S with type key = ty
 
 val ts_equal : tysymbol -> tysymbol -> bool

src/driver/whyconf.ml

@@ -93,16 +93,16 @@ module Prover = struct
       5 * Hashtbl.hash s1.prover_altern
 end
 
-module Mprover = Map.Make(Prover)
-module Sprover = Mprover.Set
-module Hprover = XHashtbl.Make(Prover)
+module Mprover = Extmap.Make(Prover)
+module Sprover = Extset.MakeOfMap(Mprover)
+module Hprover = Exthtbl.Make(Prover)
 
 module Editor = struct
   type t = string
   let compare = Pervasives.compare
 end
 
-module Meditor = Map.Make(Editor)
+module Meditor = Extmap.Make(Editor)
 
 (* Configuration file *)
 

src/driver/whyconf.mli

@@ -100,9 +100,9 @@ val prover_parseable_format : prover -> string
 
 (** Printer for prover *)
 module Prover   : OrderedHashedType with type t = prover
-module Mprover  : Map.S with type key = prover
-module Sprover  : Mprover.Set
-module Hprover  : XHashtbl.S with type key = prover
+module Mprover  : Extmap.S with type key = prover
+module Sprover  : Extset.S with module M = Mprover
+module Hprover  : Exthtbl.S with type key = prover
 
 (** {3 Prover configuration} *)
 
@@ -144,7 +144,7 @@ type config_editor = {
   editor_options : string list;
 }
 
-module Meditor : Map.S with type key = string
+module Meditor : Extmap.S with type key = string
 
 val set_editors : config -> config_editor Meditor.t -> config
 (** replace the set of editors *)

src/session/session.ml

@@ -70,13 +70,13 @@ module Pos = struct
   let hash x = Hashtbl.hash (x : t)
 end
 
-module Mpos = Map.Make(Pos)
-module Spos = Mpos.Set
-module Hpos = XHashtbl.Make(Pos)
+module Mpos = Extmap.Make(Pos)
+module Spos = Extset.MakeOfMap(Mpos)
+module Hpos = Exthtbl.Make(Pos)
 
 type meta_args = meta_arg list
 
-module Mmeta_args = Map.Make(struct
+module Mmeta_args = Extmap.Make(struct
   type t = meta_args
 
   let meta_arg_id = function
@@ -100,11 +100,12 @@ module Mmeta_args = Map.Make(struct
 
   let compare = Lists.compare compare_meta_arg
 end)
-module Smeta_args = Mmeta_args.Set
+
+module Smeta_args = Extset.MakeOfMap(Mmeta_args)
 
 type metas_args = Smeta_args.t Mstr.t
 
-module Mmetas_args = Map.Make(struct
+module Mmetas_args = Extmap.Make(struct
   type t = metas_args
   let compare = Mstr.compare Smeta_args.compare
 end)

src/session/session.mli

@@ -21,8 +21,8 @@ open Stdlib
 val debug : Debug.flag
 (** The debug flag "session" *)
 
-module PHstr : XHashtbl.Private with type key = string
-module PHprover : XHashtbl.Private with type key = Whyconf.prover
+module PHstr : Exthtbl.Private with type key = string
+module PHprover : Exthtbl.Private with type key = Whyconf.prover
 
 (** {2 Proof attempts} *)
 
@@ -54,11 +54,11 @@ type ident_path =
   }
 
 type meta_args = Theory.meta_arg list
-module Mmeta_args : Map.S with type key = meta_args
-module Smeta_args : Mmeta_args.Set
+module Mmeta_args : Extmap.S with type key = meta_args
+module Smeta_args : Extset.S with module M = Mmeta_args
 
-type metas_args =  Smeta_args.t Mstr.t
-module Mmetas_args : Map.S with type key = metas_args
+type metas_args = Smeta_args.t Mstr.t
+module Mmetas_args : Extmap.S with type key = metas_args
 
 type idpos = {
   idpos_ts : ident_path Ty.Mts.t;

src/transform/discriminate.ml

@@ -65,7 +65,7 @@ module OHTyl = OrderedHashedList(struct
   let tag = ty_hash
 end)
 
-module Mtyl = Stdlib.Map.Make(OHTyl)
+module Mtyl = Extmap.Make(OHTyl)
 
 module Lsmap = struct
 

src/transform/encoding_instantiate.ml

@@ -40,8 +40,8 @@ module OHTyl = OrderedHashedList(struct
   let tag = ty_hash
 end)
 
-module Mtyl = Map.Make(OHTyl)
-module Htyl = Hashtbl.Make(OHTyl)
+module Mtyl = Extmap.Make(OHTyl)
+module Htyl = Exthtbl.Make(OHTyl)
 
 type tenv =
   | Complete (* The transformation keep the polymorphism *)

src/transform/induction.ml

@@ -76,8 +76,8 @@ module VsList = Stdlib.OrderedHashedList(struct
   type t = vsymbol
   let tag = vs_hash
 end)
-module Mvsl = Stdlib.Map.Make(VsList)
-module Svsl = Mvsl.Set
+module Mvsl = Extmap.Make(VsList)
+module Svsl = Extset.MakeOfMap(Mvsl)
 
 (* DEBUGGING AND PRINTING *)
 

src/util/exthtbl.ml

@@ -36,22 +36,8 @@ sig
   val is_empty : 'a t -> bool
 end
 
-module type Hashtbl =
-sig
-val hash : 'a -> int
-module type S = S
-module type Private = Private
-module Make (X:Hashtbl.HashedType) : S with type key = X.t
-end
-
-module Hashtbl =
-struct
-
 let hash = Hashtbl.hash
 
-module type S = S
-module type Private = Private
-
 module Make (X:Hashtbl.HashedType) : S with type key = X.t =
 struct
   module M = Hashtbl.Make(X)
@@ -78,4 +64,3 @@ struct
 
   let is_empty h = length h = 0
 end
-end

src/util/exthtbl.mli

@@ -9,10 +9,8 @@
 (*                                                                  *)
 (********************************************************************)
 
-module type Hashtbl =
-sig
-
 val hash : 'a -> int
+  (** the same as Hashtbl.hash *)
 
 module type S =
 sig
@@ -75,7 +73,3 @@ sig
 end
 
 module Make (X:Hashtbl.HashedType) : S with type key = X.t
-
-end
-
-module Hashtbl : Hashtbl

src/util/extmap.ml

@@ -60,6 +60,8 @@ module type S =
     val set_diff : 'a t -> 'b t -> 'a t
     val set_submap : 'a t -> 'b t -> bool
     val set_disjoint : 'a t -> 'b t -> bool
+    val set_compare : 'a t -> 'b t -> int
+    val set_equal : 'a t -> 'b t -> bool
     val find_def : 'a -> key -> 'a t -> 'a
     val find_opt : key -> 'a t -> 'a option
     val find_exn : exn -> key -> 'a t -> 'a
@@ -67,6 +69,7 @@ module type S =
     val mapi_filter: (key -> 'a -> 'b option) -> 'a t -> 'b t
     val mapi_fold:
       (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
+    val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
     val fold2_inter: (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
     val fold2_union:
       (key -> 'a option -> 'b option -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
@@ -76,68 +79,16 @@ module type S =
     val add_new : exn -> key -> 'a -> 'a t -> 'a t
     val keys: 'a t -> key list
     val values: 'a t -> 'a list
+    val of_list : (key * 'a) list -> 'a t
     type 'a enumeration
     val val_enum : 'a enumeration -> (key * 'a) option
     val start_enum : 'a t -> 'a enumeration
     val next_enum : 'a enumeration -> 'a enumeration
     val start_ge_enum : key -> 'a t -> 'a enumeration
     val next_ge_enum : key -> 'a enumeration -> 'a enumeration
-    val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
-    val of_list : (key * 'a) list -> 'a t
-
-    module type Set =
-      sig
-        type elt = key
-        type set = unit t
-        type t = set
-        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 merge: (elt -> bool -> bool -> bool) -> t -> t -> t
-        val compare: t -> t -> int
-        val equal: t -> t -> bool
-        val subset: t -> t -> bool
-        val disjoint: 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
-        val change : (bool -> bool) -> elt -> t -> t
-        val union : t -> t -> t
-        val inter : t -> t -> t
-        val diff : t -> t -> t
-        val fold2:  (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
-        val translate : (elt -> elt) -> t -> t
-        val add_new : exn -> elt -> t -> t
-        val is_num_elt : int -> t -> bool
-        val fold_left: ('b -> elt -> 'b) -> 'b -> t -> 'b
-        val of_list : elt list -> t
-      end
-
-    module Set : Set
   end
 
-module type Map = sig
-  module type OrderedType = Map.OrderedType
-  module type S = S
-  module Make (Ord : OrderedType) : S with type key = Ord.t
-end
-
-module Map =
-struct
   module type OrderedType = Map.OrderedType
-  module type S = S
 
   module Make(Ord: OrderedType) = struct
     type key = Ord.t
@@ -521,7 +472,8 @@ struct
     let set_diff m1 m2 = diff (fun _ _ _ -> None) m1 m2
     let set_submap m1 m2 = submap (fun _ _ _ -> true) m1 m2
     let set_disjoint m1 m2 = disjoint (fun _ _ _ -> false) m1 m2
-
+    let set_compare m1 m2 = compare (fun _ _ -> 0) m1 m2
+    let set_equal m1 m2 = equal (fun _ _ -> true) m1 m2
 
     let rec find_def def x = function
         Empty -> def
@@ -672,91 +624,4 @@ struct
     let of_list l =
       List.fold_left (fun acc (k,d) -> add k d acc) empty l
 
-    module type Set =
-      sig
-        type elt = key
-        type set = unit t
-        type t = set
-        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 merge: (elt -> bool -> bool -> bool) -> t -> t -> t
-        val compare: t -> t -> int
-        val equal: t -> t -> bool
-        val subset: t -> t -> bool
-        val disjoint: 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
-        val change : (bool -> bool) -> elt -> t -> t
-        val union : t -> t -> t
-        val inter : t -> t -> t
-        val diff : t -> t -> t
-        val fold2:  (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
-        val translate : (elt -> elt) -> t -> t
-        val add_new : exn -> elt -> t -> t
-        val is_num_elt : int -> t -> bool
-        val fold_left: ('b -> elt -> 'b) -> 'b -> t -> 'b
-        val of_list : elt list -> t
-      end
-
-    module Set =
-      struct
-        type elt = Ord.t
-        type set = unit t
-        type t = set
-
-        let is_true b = if b then Some () else None
-        let is_some o = o <> None
-        let const f e _ = f e
-
-        let empty = empty
-        let is_empty = is_empty
-        let mem = mem
-        let add e s = add e () s
-        let singleton e = singleton e ()
-        let remove = remove
-        let merge f = merge (fun e a b ->
-          is_true (f e (is_some a) (is_some b)))
-        let compare = compare (fun _ _ -> 0)
-        let equal = equal (fun _ _ -> true)
-        let subset = submap (fun _ _ _ -> true)
-        let disjoint = disjoint (fun _ _ _ -> false)
-        let iter f = iter (const f)
-        let fold f = fold (const f)
-        let for_all f = for_all (const f)
-        let exists f = exists (const f)
-        let filter f = filter (const f)
-        let partition f = partition (const f)
-        let cardinal = cardinal
-        let elements = keys
-        let min_elt t = fst (min_binding t)
-        let max_elt t = fst (max_binding t)
-        let choose t = fst (choose t)
-        let split e t = let l,m,r = split e t in l,(m <> None),r
-        let change f x s = change (fun a -> is_true (f (is_some a))) x s
-        let union = union (fun _ _ _ -> Some ())
-        let inter = inter (fun _ _ _ -> Some ())
-        let diff = diff (fun _ _ _ -> None)
-        let fold2 f = fold2_union (fun k _ _ acc -> f k acc)
-        let translate = translate
-        let add_new e x s = add_new e x () s
-        let is_num_elt n m = is_num_elt n m
-        let fold_left f = fold_left (fun accu k () -> f accu k)
-        let of_list l =
-          List.fold_left (fun acc a -> add a acc) empty l
-      end
   end
-end

src/util/extmap.mli

@@ -12,12 +12,10 @@
 (***********************************************************************)
 
 (* This file originates from the OCaml v 3.12 Standard Library.
-   It was extended and modified for the needs of the Why3 project
-   by François Bobot and Andrei Paskevich. It is distributed under
-   the terms of its initial license, which is provided in file
-   OCAML-LICENSE. *)
+   It was extended and modified for the needs of the Why3 project.
+   It is distributed under the terms of its initial license, which
+   is provided in the file OCAML-LICENSE. *)
 
-module type Map = sig
   (** Association tables over ordered types.
 
      This module implements applicative association tables, also known as
@@ -28,10 +26,10 @@ module type Map = sig
      and insertion take time logarithmic in the size of the map.
   *)
 
-  (** Input signature of the functor {!Map.Make}. *)
+  (** Input signature of the functor {!Extmap.Make}. *)
   module type OrderedType = Map.OrderedType
 
-  (** Output signature of the functor {!Map.Make}. *)
+  (** Output signature of the functor {!Extmap.Make}. *)
   module type S =
   sig
     type key
@@ -57,8 +55,7 @@ module type Map = sig
 
     val singleton: key -> 'a -> 'a t
     (** [singleton x y] returns the one-element map that contains a binding [y]
-        for [x].
-        @since 3.12.0 *)
+        for [x]. *)
 
     val remove: key -> 'a t -> 'a t
     (** [remove x m] returns a map containing the same bindings as
@@ -68,8 +65,7 @@ module type Map = sig
          (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
     (** [merge f m1 m2] computes a map whose keys is a subset of keys of [m1]
         and of [m2]. The presence of each such binding, and the corresponding
-        value, is determined with the function [f].
-        @since 3.12.0 *)
+        value, is determined with the function [f]. *)
 
     val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
     (** Total ordering between maps.  The first argument is a total ordering
@@ -94,53 +90,44 @@ module type Map = sig
 
     val for_all: (key -> 'a -> bool) -> 'a t -> bool
     (** [for_all p m] checks if all the bindings of the map
-        satisfy the predicate [p].
-        @since 3.12.0 *)
+        satisfy the predicate [p]. *)
 
     val exists: (key -> 'a -> bool) -> 'a t -> bool
     (** [exists p m] checks if at least one binding of the map
-        satisfy the predicate [p].
-        @since 3.12.0 *)
+        satisfy the predicate [p]. *)
 
     val filter: (key -> 'a -> bool) -> 'a t -> 'a t
     (** [filter p m] returns the map with all the bindings in [m]
-        that satisfy predicate [p].
-        @since 3.12.0 *)
+        that satisfy predicate [p]. *)
 
     val partition: (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
     (** [partition p m] returns a pair of maps [(m1, m2)], where
         [m1] contains all the bindings of [s] that satisfy the
         predicate [p], and [m2] is the map with all the bindings of
-        [s] that do not satisfy [p].
-        @since 3.12.0 *)
+        [s] that do not satisfy [p]. *)
 
     val cardinal: 'a t -> int
-    (** Return the number of bindings of a map.
-        @since 3.12.0 *)
+    (** Return the number of bindings of a map. *)
 
     val bindings: 'a t -> (key * 'a) list
     (** Return the list of all bindings of the given map.
         The returned list is sorted in increasing order with respect
         to the ordering [Ord.compare], where [Ord] is the argument
-        given to {!Map.Make}.
-        @since 3.12.0 *)
+        given to {!Extmap.Make}. *)
 
     val min_binding: 'a t -> (key * 'a)
     (** Return the smallest binding of the given map
         (with respect to the [Ord.compare] ordering), or raise
-        [Not_found] if the map is empty.
-        @since 3.12.0 *)
+        [Not_found] if the map is empty. *)
 
     val max_binding: 'a t -> (key * 'a)
-    (** Same as {!Map.S.max_binding}, but returns the largest
-        binding of the given map.
-        @since 3.12.0 *)
+    (** Same as {!Extmap.S.min_binding}, but returns the largest
+        binding of the given map. *)
 
     val choose: 'a t -> (key * 'a)
     (** Return one binding of the given map, or raise [Not_found] if
         the map is empty. Which binding is chosen is unspecified,
-        but equal bindings will be chosen for equal maps.
-        @since 3.12.0 *)
+        but equal bindings will be chosen for equal maps. *)
 
     val split: key -> 'a t -> 'a t * 'a option * 'a t
     (** [split x m] returns a triple [(l, data, r)], where
@@ -149,8 +136,7 @@ module type Map = sig
           [r] is the map with all the bindings of [m] whose key
         is strictly greater than [x];
           [data] is [None] if [m] contains no binding for [x],
-          or [Some v] if [m] binds [v] to [x].
-        @since 3.12.0 *)
+          or [Some v] if [m] binds [v] to [x]. *)
 
     val find: key -> 'a t -> 'a
     (** [find x m] returns the current binding of [x] in [m],
@@ -164,10 +150,10 @@ module type Map = sig
         with respect to the ordering over the type of the keys. *)
 
     val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
-    (** Same as {!Map.S.map}, but the function receives as arguments both
+    (** Same as {!Extmap.S.map}, but the function receives as arguments both
         the key and the associated value for each binding of the map. *)
 
-    (** Added into why stdlib version *)
+    (** @Added in Why3 *)
 
     val is_num_elt : int -> 'a t -> bool
     (** check if the map has the given number of elements *)
@@ -222,6 +208,12 @@ module type Map = sig
     val set_disjoint : 'a t -> 'b t -> bool
     (** [set_disjoint = disjoint (fun _ _ _ -> false)] *)
 
+    val set_compare : 'a t -> 'b t -> int
+    (** [set_compare = compare (fun _ _ -> 0)] *)
+
+    val set_equal : 'a t -> 'b t -> bool
+    (** [set_equal = equal (fun _ _ -> true)] *)
+
     val find_def : 'a -> key -> 'a t -> 'a
     (** [find_def x d m] returns the current binding of [x] in [m],
         or return [d] if no such binding exists. *)
@@ -235,15 +227,18 @@ module type Map = sig
         of [x] in [m], or raise [exn] if no such binding exists. *)
 
     val map_filter: ('a -> 'b option) -> 'a t -> 'b t
-    (** Same as {!Map.S.map}, but may remove bindings. *)
+    (** Same as {!Extmap.S.map}, but may remove bindings. *)