diff --git a/Makefile.in b/Makefile.in
index 796b7d320e070d6edc7e1f3f9b8ffd9a3b3065ea..f60ca34c99a9c61680ac125b8fce3e1b24637952 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -165,8 +165,8 @@ LIBGENERATED = src/util/config.ml \
 	       lib/ocaml/why3__BigInt_compat.ml
 
 LIB_UTIL = config bigInt util opt lists strings \
-	   extmap extset exthtbl weakhtbl \
-	   hashcons stdlib exn_printer pp json debug loc lexlib print_tree \
+	   pp extmap extset exthtbl weakhtbl \
+	   hashcons stdlib exn_printer json debug loc lexlib print_tree \
 	   cmdline warning sysutil rc plugin bigInt number pqueue
 
 LIB_CORE = ident ty term pattern decl coercion theory \
diff --git a/src/util/extset.ml b/src/util/extset.ml
index 5523b29fa3e6e8b48d0a7a5ede97671ebaf0f59f..0e86ad9f239dd987713831d2c8e051b2c60cde95 100644
--- a/src/util/extset.ml
+++ b/src/util/extset.ml
@@ -50,6 +50,7 @@ module type S = sig
   val contains: t -> elt -> bool
   val add_left: t -> elt -> t
   val remove_left: t -> elt -> t
+  val print: (Format.formatter -> elt -> unit) -> Format.formatter -> t -> unit
 end
 
 module MakeOfMap (M: Extmap.S) = struct
@@ -97,6 +98,12 @@ module MakeOfMap (M: Extmap.S) = struct
   let contains = M.contains
   let add_left s e = M.add e () s
   let remove_left s e = M.remove e s
+  let print print_elt fmt s =
+    if is_empty s then Format.fprintf fmt "{}" else begin
+      Format.fprintf fmt "@[<hov 2>{ ";
+      Pp.print_iter1 iter Pp.comma print_elt fmt s;
+      Format.fprintf fmt "}@]"
+    end
 end
 
 module type OrderedType = Set.OrderedType
diff --git a/src/util/extset.mli b/src/util/extset.mli
index c1e933e4faff5f6e1c0e77d896429fa4a369cc8a..d928589c7f666bf59fe987572fb18b61c4e1252c 100644
--- a/src/util/extset.mli
+++ b/src/util/extset.mli
@@ -170,6 +170,9 @@ module type S =
 
     val remove_left: t -> elt -> t
     (** [remove_left s x] is the same as [remove x s]. *)
+
+    val print: (Format.formatter -> elt -> unit) ->
+               Format.formatter -> t -> unit
   end
 
 module MakeOfMap (M : Extmap.S) : S with module M = M