diff --git a/Makefile.in b/Makefile.in
index dee14cf83a89e41cfb01e2e2a68881d2e362bbf4..0bc2d710d0b3003260d01623a76afaa15f4f85d8 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -109,7 +109,7 @@ LIBGENERATED = src/util/config.ml \
 	       src/parser/parser.mli src/parser/parser.ml \
 	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
 	       src/driver/driver_lexer.ml \
-               src/session/compress.ml src/session/xml.ml \
+	       src/session/compress.ml src/session/xml.ml \
 	       src/session/strategy_parser.ml \
 	       lib/ocaml/why3__BigInt_compat.ml
 
@@ -124,7 +124,7 @@ LIB_CORE = ident ty term pattern decl theory \
 LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
 	     whyconf autodetection
 
-LIB_MLW	= ity
+LIB_MLW = ity
 
 LIB_PARSER = ptree glob parser typing lexer
 
@@ -147,6 +147,9 @@ LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
 	    mlw_dexpr mlw_typing mlw_driver mlw_ocaml \
 	    mlw_main mlw_interp
 
+LIB_SESSION = compress xml termcode session session_tools strategy \
+              strategy_parser session_scheduler
+
 LIBMODULES =  $(addprefix src/util/, $(LIB_UTIL)) \
 	      $(addprefix src/core/, $(LIB_CORE)) \
 	      $(addprefix src/driver/, $(LIB_DRIVER)) \
@@ -154,50 +157,30 @@ LIBMODULES =  $(addprefix src/util/, $(LIB_UTIL)) \
 	      $(addprefix src/parser/, $(LIB_PARSER)) \
 	      $(addprefix src/transform/, $(LIB_TRANSFORM)) \
 	      $(addprefix src/printer/, $(LIB_PRINTER)) \
-	      $(addprefix src/whyml/, $(LIB_WHYML))
+	      $(addprefix src/whyml/, $(LIB_WHYML)) \
+	      $(addprefix src/session/, $(LIB_SESSION))
 
-LIB_SESSION = compress xml termcode session session_tools strategy \
-              strategy_parser session_scheduler
-
-LIBSESSIONMODULES = $(addprefix src/session/, $(LIB_SESSION))
-
-LIBDIRS = util core driver mlw parser transform printer whyml
+LIBDIRS = util core driver mlw parser transform printer whyml session
 LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
 
-LIBSESSIONDIRS = session
-LIBSESSIONINCLUDES = $(addprefix -I src/, $(LIBSESSIONDIRS))
-
 LIBDEP = $(addsuffix .dep, $(LIBMODULES))
 LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
 LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
 
-LIBSESSIONDEP = $(addsuffix .dep, $(LIBSESSIONMODULES))
-LIBSESSIONCMO = $(addsuffix .cmo, $(LIBSESSIONMODULES))
-LIBSESSIONCMX = $(addsuffix .cmx, $(LIBSESSIONMODULES))
-
 $(LIBDEP): DEPFLAGS += $(LIBINCLUDES)
 $(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
 $(LIBCMX): OFLAGS += -for-pack Why3
 
-$(LIBSESSIONDEP): DEPFLAGS += $(LIBSESSIONINCLUDES)
-$(LIBSESSIONCMO) $(LIBSESSIONCMX): INCLUDES += $(LIBSESSIONINCLUDES)
-$(LIBSESSIONCMX): OFLAGS += -for-pack Why3session
-
 $(LIBDEP): $(LIBGENERATED)
-$(LIBSESSIONDEP): $(LIBGENERATED)
 
 # Zarith
 
 ifeq (@enable_zarith@,yes)
-
 lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_zarith.ml
 	cp lib/ocaml/why3__BigInt_zarith.ml $@
-
 else
-
 lib/ocaml/why3__BigInt_compat.ml: config.status lib/ocaml/why3__BigInt_num.ml
 	cp lib/ocaml/why3__BigInt_num.ml $@
-
 endif
 
 clean::
@@ -206,15 +189,11 @@ clean::
 # Ocamlzip
 
 ifeq (@enable_zip@,yes)
-
 src/session/compress.ml: config.status src/session/compress_z.ml
 	cp src/session/compress_z.ml $@
-
 else
-
 src/session/compress.ml: config.status src/session/compress_none.ml
 	cp src/session/compress_none.ml $@
-
 endif
 
 clean::
@@ -241,32 +220,13 @@ lib/why3/why3.cmx: $(LIBCMX)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
 
-byte: lib/why3/why3session.cma
-opt:  lib/why3/why3session.cmxa
-
-lib/why3/why3session.cma: lib/why3/why3session.cmo
-	$(if $(QUIET),@echo 'Linking  $@' &&) \
-	    $(OCAMLC) -a $(BFLAGS) -o $@ $^
-
-lib/why3/why3session.cmxa: lib/why3/why3session.cmx
-	$(if $(QUIET),@echo 'Linking  $@' &&) \
-	    $(OCAMLOPT) -a $(OFLAGS) -o $@ $^
-
-lib/why3/why3session.cmo: $(LIBSESSIONCMO)
-	$(if $(QUIET),@echo 'Linking  $@' &&) \
-	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^
-
-lib/why3/why3session.cmx: $(LIBSESSIONCMX)
-	$(if $(QUIET),@echo 'Linking  $@' &&) \
-	    $(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
-
 # clean and depend
 
 ifneq "$(MAKECMDGOALS)" "clean"
-include $(LIBDEP) $(LIBSESSIONDEP)
+include $(LIBDEP)
 endif
 
-depend: $(LIBDEP) $(LIBSESSIONDEP)
+depend: $(LIBDEP)
 
 LIBSDIRS = src $(addprefix src/, $(LIBDIRS))
 LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
@@ -279,7 +239,7 @@ LIBCLEAN = $(addsuffix /*.cm[iox], $(LIBSDIRS)) \
 
 clean::
 	rm -f $(LIBCLEAN) $(LIBGENERATED)
-	rm -f lib/why3/why3.cm* lib/why3/why3.[ao]
+	rm -f lib/why3/why3session.* lib/why3/why3.cm* lib/why3/why3.[ao]
 
 ###############
 # installation
@@ -326,7 +286,6 @@ endif
 install_no_local_lib::
 	mkdir -p $(OCAMLINSTALLLIB)/why3
 	cp -f lib/why3/why3.cm* lib/why3/why3.[ao] \
-		lib/why3/why3session.cm* lib/why3/why3session.[ao] \
 		lib/why3/META $(OCAMLINSTALLLIB)/why3
 
 ifeq (@enable_local@,yes)
@@ -579,17 +538,17 @@ bin/why3realize.byte: lib/why3/why3.cma src/tools/why3realize.cmo
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
 
-bin/why3replay.opt: lib/why3/why3.cmxa lib/why3/why3session.cmxa src/tools/why3replay.cmx
+bin/why3replay.opt: lib/why3/why3.cmxa src/tools/why3replay.cmx
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
 
-bin/why3replay.byte: lib/why3/why3.cma lib/why3/why3session.cma src/tools/why3replay.cmo
+bin/why3replay.byte: lib/why3/why3.cma src/tools/why3replay.cmo
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
 
 clean_old_install::
 	rm -f $(TOOLS_BIN:%=$(TOOLDIR)/%$(EXE)) $(BINDIR)/why3$(EXE)
-	rm -f $(BINDIR)/why3config$(EXE) $(BINDIR)/why3bench$(EXE) $(BINDIR)/why3replayer$(EXE) 
+	rm -f $(BINDIR)/why3bench$(EXE) $(BINDIR)/why3replayer$(EXE)
 
 install_no_local::
 	cp -f bin/why3.@OCAMLBEST@ $(BINDIR)/why3$(EXE)
@@ -721,11 +680,11 @@ opt:  bin/why3ide.opt
 bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
 bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
 
-bin/why3ide.opt: lib/why3/why3.cmxa lib/why3/why3session.cmxa src/ide/resetgc.o $(IDECMX)
+bin/why3ide.opt: lib/why3/why3.cmxa src/ide/resetgc.o $(IDECMX)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
 
-bin/why3ide.byte: lib/why3/why3.cma lib/why3/why3session.cma src/ide/resetgc.o $(IDECMO)
+bin/why3ide.byte: lib/why3/why3.cma src/ide/resetgc.o $(IDECMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^
 
@@ -780,11 +739,11 @@ $(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session
 byte: bin/why3session.byte
 opt:  bin/why3session.opt
 
-bin/why3session.opt: lib/why3/why3.cmxa lib/why3/why3session.cmxa $(SESSIONCMX)
+bin/why3session.opt: lib/why3/why3.cmxa $(SESSIONCMX)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
 
-bin/why3session.byte: lib/why3/why3.cma lib/why3/why3session.cma $(SESSIONCMO)
+bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
 
@@ -844,11 +803,11 @@ src/coq-tactic/coqCompat.ml: src/coq-tactic/coqCompat@coq_compat_version@.ml
 
 lib/coq-tactic/why3tac.cmxs: lib/why3/why3.cmxa $(COQPCMX)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
-	    $(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
+	    $(OCAMLOPT) $(OFLAGS) -o $@ -shared $(addsuffix .cmxa, @ZIPLIB@) $^
 
 lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
-	    $(OCAMLC) -a $(BFLAGS) -o $@ $^
+	    $(OCAMLC) -a $(BFLAGS) -o $@ $(addsuffix .cma, @ZIPLIB@) $^
 
 src/coq-tactic/g_why3tac.ml: src/coq-tactic/g_why3tac.ml4
 	$(if $(QUIET),@echo 'Camlp5   $<' &&) \
@@ -1559,16 +1518,16 @@ test-api-mlw.opt: examples/use_api/mlw.ml lib/why3/why3.cmxa
 #test-shape: lib/why3/why3.cma
 #	ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) $? examples/test_shape.ml
 
-test-session.byte: examples/use_api/create_session.ml lib/why3/why3.cma lib/why3/why3session.cma
+test-session.byte: examples/use_api/create_session.ml lib/why3/why3.cma
 	$(if $(QUIET),@echo 'Ocaml    $<' &&) \
-	ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma lib/why3/why3session.cma $< > /dev/null\
+	ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\
 	|| (rm -f why3session.xml why3shapes why3shapes.gz;  \
 	printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
 	@rm -f why3session.xml why3shapes why3shapes.gz
 
-test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa lib/why3/why3session.cmxa
+test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
 	$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
-	($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa lib/why3/why3session.cmxa  $< \
+	($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa  $< \
 	&& ./test-session.opt > /dev/null) \
 	|| (rm -f test-session.opt why3session.xml why3shapes why3shapes.gz; \
 	printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
@@ -1692,8 +1651,7 @@ doc/apidoc:
 
 apidoc: doc/apidoc $(FILESTODOC)
 	$(OCAMLDOC) -d doc/apidoc -html -t "Why3 API documentation" \
-		-keep-code $(INCLUDES) \
-		$(LIBINCLUDES) $(LIBSESSIONINCLUDES) -I lib/why3 $(FILESTODOC)
+		-keep-code $(INCLUDES) $(LIBINCLUDES) -I lib/why3 $(FILESTODOC)
 
 # could we include also the dependency graph ? -- someone
 # At least we can give a way to create it -- francois
diff --git a/examples/use_api/create_session.ml b/examples/use_api/create_session.ml
index ab2730d99e94287bcdaad3f7f156cbc7a00add81..186d3af5bf9ba933325a5fac27c6f336ec8d0d43 100644
--- a/examples/use_api/create_session.ml
+++ b/examples/use_api/create_session.ml
@@ -13,7 +13,7 @@
 
 This file builds a new session from a given file.
 
-To each goal is added as many proof attempts as provers 
+To each goal is added as many proof attempts as provers
 found in the configuration.
 
 
@@ -23,9 +23,6 @@ open Format
 
 (* opening the Why3 library *)
 open Why3
-(* opening the Why3 session library *)
-open Why3session
-
 
 (* access to the Why configuration *)
 
@@ -63,11 +60,11 @@ let keygen ?parent () = ()
 (* create an empty session in the current directory *)
 let env_session,_,_ =
   let dummy_session : unit Session.session = Session.create_session "." in
-  Session.update_session ~use_shapes:false ~keygen ~allow_obsolete:true 
+  Session.update_session ~use_shapes:false ~keygen ~allow_obsolete:true
     dummy_session env config
 
 (* adds a file in the new session *)
-let file : unit Session.file = 
+let file : unit Session.file =
   let file_name = "examples/logic/hello_proof.why" in
   try
     Session.add_file keygen env_session file_name
@@ -77,7 +74,7 @@ let file : unit Session.file =
     exit 1
 
 (* explore the theories in that file *)
-let theories = file.Session.file_theories 
+let theories = file.Session.file_theories
 let () = eprintf "%d theories found@." (List.length theories)
 
 (* add proof attempts for each goals in the theories *)
@@ -94,7 +91,7 @@ let add_proofs_attempts g =
           ~memlimit:1000
           ~edit:None
           g p.Whyconf.prover Session.Scheduled
-      in ()) 
+      in ())
     provers
 
 let () =
diff --git a/lib/why3/META.in b/lib/why3/META.in
index 5462873b9bf6c9868df8d2b36f74537c0c64d2dc..fc56b0530db7a988a2ecb55c939372ece3aff243 100644
--- a/lib/why3/META.in
+++ b/lib/why3/META.in
@@ -2,10 +2,4 @@ description = "Why3 library"
 version = "@VERSION@"
 archive(byte) = "why3.cma"
 archive(native) = "why3.cmxa"
-requires = "str unix num dynlink"
-
-description = "Why3 session library"
-version = "@VERSION@"
-archive(byte) = "why3session.cma"
-archive(native) = "why3session.cmxa"
-requires = "str unix num dynlink @ZIPLIB@ why3"
+requires = "str unix num dynlink @ZIPLIB@"
diff --git a/lib/why3/why3session.ml b/lib/why3/why3session.ml
deleted file mode 100644
index e14a7c4a07952e9e1b2eee2da4f2cd62b8efe5c9..0000000000000000000000000000000000000000
--- a/lib/why3/why3session.ml
+++ /dev/null
@@ -1 +0,0 @@
-(* This file is a stub for ocamldep. Do not delete it. *)
diff --git a/src/ide/gconfig.ml b/src/ide/gconfig.ml
index 2244fb83137e9da7b87fc3469eca66284ac22069..c082eb2d24763ae47392d4a7e34f2ecc9c3e3cb4 100644
--- a/src/ide/gconfig.ml
+++ b/src/ide/gconfig.ml
@@ -12,7 +12,6 @@
 open Why3
 open Rc
 open Whyconf
-open Why3session
 
 let debug = Debug.register_info_flag "ide_info"
   ~desc:"Print@ why3ide@ debugging@ messages."
diff --git a/src/ide/gconfig.mli b/src/ide/gconfig.mli
index ecb36cdb697405eb702d1d8b88652a293d5ec650..a9fae70a5cd96a6ce37da373583a8c9e8b2b93ab 100644
--- a/src/ide/gconfig.mli
+++ b/src/ide/gconfig.mli
@@ -10,7 +10,6 @@
 (********************************************************************)
 
 open Why3
-open Why3session
 
 type t =
     { mutable window_width : int;
diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml
index e709788c3f7901b53cd69746b850cd1f44481b09..dc34d311e5f9d4d8c9327defffd1d4375bf6f062 100644
--- a/src/ide/gmain.ml
+++ b/src/ide/gmain.ml
@@ -18,8 +18,6 @@ open Gconfig
 open Stdlib
 open Debug
 
-open Why3session
-
 module C = Whyconf
 
 external reset_gc : unit -> unit = "ml_reset_gc"
diff --git a/src/session/session.ml b/src/session/session.ml
index f4141bc985446b5af656428cf87b9c40124ecfe8..6bf2bc9dd1d300682aabab8e577bfb570a1437d3 100644
--- a/src/session/session.ml
+++ b/src/session/session.ml
@@ -9,7 +9,6 @@
 (*                                                                  *)
 (********************************************************************)
 
-open Why3
 open Stdlib
 open Ty
 open Ident
diff --git a/src/session/session.mli b/src/session/session.mli
index db4dd503cda4d1ff566c247c5b379900eb865c9e..6156eca2f0bdc0916c0f351a5e2b763fbf4687b8 100644
--- a/src/session/session.mli
+++ b/src/session/session.mli
@@ -9,8 +9,6 @@
 (*                                                                  *)
 (********************************************************************)
 
-open Why3
-
 (** Proof sessions
 
     Define all the functions needed for managing a session:
diff --git a/src/session/session_scheduler.ml b/src/session/session_scheduler.ml
index 37ae33f88a06c5d9f0c29f10123c33eeea0d12bc..9c947fde237c02df381fa71803aea454dd9ddc6f 100644
--- a/src/session/session_scheduler.ml
+++ b/src/session/session_scheduler.ml
@@ -10,7 +10,6 @@
 (********************************************************************)
 
 open Format
-open Why3
 open Session
 
 let debug = Debug.register_info_flag "scheduler"
diff --git a/src/session/session_scheduler.mli b/src/session/session_scheduler.mli
index 51fc0782706965aa9c08d8bf0976c0979730aa91..9850e95f3d81b7451abb9530ed1958a456d06da0 100644
--- a/src/session/session_scheduler.mli
+++ b/src/session/session_scheduler.mli
@@ -30,7 +30,6 @@ module Todo : sig
 
 end
 
-open Why3
 open Session
 
 (** {2 Observers signature} *)
diff --git a/src/session/session_tools.ml b/src/session/session_tools.ml
index e038940faad472be3c587b2385fe6e63740bd870..09184682d63797b5bb4b66e5675300e5eb78983f 100644
--- a/src/session/session_tools.ml
+++ b/src/session/session_tools.ml
@@ -9,7 +9,6 @@
 (*                                                                  *)
 (********************************************************************)
 
-open Why3
 open Whyconf
 open Session
 
diff --git a/src/session/session_tools.mli b/src/session/session_tools.mli
index 9ef4b1b92633ff39bbd93901080b9127720a5098..a7421153eb6518b377a08dc50fecb1df1a52bef3 100644
--- a/src/session/session_tools.mli
+++ b/src/session/session_tools.mli
@@ -11,7 +11,6 @@
 
 (** Generic tools that can be applied on sessions *)
 
-open Why3
 open Session
 
 val unknown_to_known_provers  :
diff --git a/src/session/termcode.ml b/src/session/termcode.ml
index e9f5c8d5caba21d8015a3494a4962b31c95028dd..787ba1f1eeab8173697ca7b5bf42b3f785464a5d 100644
--- a/src/session/termcode.ml
+++ b/src/session/termcode.ml
@@ -9,7 +9,6 @@
 (*                                                                  *)
 (********************************************************************)
 
-open Why3
 open Term
 
 (*******************************)
diff --git a/src/session/termcode.mli b/src/session/termcode.mli
index f9f03cf642efe67e8d55a315aaacf179294f0f5c..ee8e5df31125f3b8d7c460cf2702a42e6536a5da 100644
--- a/src/session/termcode.mli
+++ b/src/session/termcode.mli
@@ -9,8 +9,6 @@
 (*                                                                  *)
 (********************************************************************)
 
-open Why3
-
 (** Explanations *)
 
 val goal_expl_task:
diff --git a/src/session/xml.mll b/src/session/xml.mll
index e1050869b6fce8ef2ba8f8f8251a527fc056d659..10aa171b7e24f65166dcf004187230e48b677d56 100644
--- a/src/session/xml.mll
+++ b/src/session/xml.mll
@@ -46,7 +46,7 @@
 
   let parse_error s = raise (Parse_error s)
 
-  let debug = Why3.Debug.register_info_flag "xml"
+  let debug = Debug.register_info_flag "xml"
     ~desc:"Print@ the@ XML@ parser@ debugging@ messages."
 }
 
@@ -68,7 +68,7 @@ rule xml_prolog fixattrs = parse
 | "<?xml" space+ "version=\"1.0\"" space+ "encoding=\"UTF-8\"" space+ "?>"
     { xml_doctype fixattrs "1.0" "" lexbuf }
 | "<?xml" ([^'?']|'?'[^'>'])* "?>"
-    { Why3.Debug.dprintf debug "[Xml warning] prolog ignored@.";
+    { Debug.dprintf debug "[Xml warning] prolog ignored@.";
       xml_doctype fixattrs "1.0" "" lexbuf }
 | _
     { parse_error "wrong prolog" }
@@ -98,26 +98,26 @@ and elements fixattrs group_stack element_stack = parse
   | "</" (ident as celem) space* '>'
       { match group_stack with
          | [] ->
-             Why3.Debug.dprintf debug
+             Debug.dprintf debug
                "[Xml warning] unexpected closing Xml element `%s'@."
                celem;
              elements fixattrs group_stack element_stack lexbuf
          | (elem,att,stack)::g ->
              if celem <> elem then
-               Why3.Debug.dprintf debug
+               Debug.dprintf debug
                  "[Xml warning] Xml element `%s' closed by `%s'@."
                  elem celem;
              let e = mk_element elem att element_stack in
              elements fixattrs g (e::stack) lexbuf
        }
   | '<'
-      { Why3.Debug.dprintf debug "[Xml warning] unexpected '<'@.";
+      { Debug.dprintf debug "[Xml warning] unexpected '<'@.";
         elements fixattrs group_stack element_stack lexbuf }
   | eof
       { match group_stack with
          | [] -> element_stack
          | (elem,_,_)::_ ->
-             Why3.Debug.dprintf debug "[Xml warning] unclosed Xml element `%s'@." elem;
+             Debug.dprintf debug "[Xml warning] unclosed Xml element `%s'@." elem;
              pop_all group_stack element_stack
       }
   | _ as c
diff --git a/src/tools/why3replay.ml b/src/tools/why3replay.ml
index ad2b64d6fd0b4db37510c22b625894a5f1767547..0f3f7bb8f400e5dea7e37d360f2f5b3f58ddc962 100644
--- a/src/tools/why3replay.ml
+++ b/src/tools/why3replay.ml
@@ -11,7 +11,6 @@
 
 open Format
 open Why3
-open Why3session
 
 (** {2 Warnings} *)
 
diff --git a/src/why3session/why3session_copy.ml b/src/why3session/why3session_copy.ml
index 69cc5a459531b97bcea774cd6ae0eff0e68fe792..72e5807c6ea0ea7d48c7bd3b4ce568f4ebd1e90d 100644
--- a/src/why3session/why3session_copy.ml
+++ b/src/why3session/why3session_copy.ml
@@ -10,7 +10,6 @@
 (********************************************************************)
 
 open Why3
-open Why3session
 open Why3session_lib
 open Whyconf
 open Session
diff --git a/src/why3session/why3session_csv.ml b/src/why3session/why3session_csv.ml
index be98135ecff15d736d3bd157740b5ae4627ed19c..230bd2bab20201286a2ce2a448cd3a57f88c360c 100644
--- a/src/why3session/why3session_csv.ml
+++ b/src/why3session/why3session_csv.ml
@@ -10,7 +10,6 @@
 (********************************************************************)
 
 open Why3
-open Why3session
 open Why3session_lib
 open Format
 
diff --git a/src/why3session/why3session_html.ml b/src/why3session/why3session_html.ml
index f088980212dc287a5da7b5eb825d1ac172897425..1e32990672677979a6cbf258c2e624634d9c3841 100644
--- a/src/why3session/why3session_html.ml
+++ b/src/why3session/why3session_html.ml
@@ -11,7 +11,6 @@
 
 open Format
 open Why3
-open Why3session
 open Why3session_lib
 
 module Hprover = Whyconf.Hprover
diff --git a/src/why3session/why3session_info.ml b/src/why3session/why3session_info.ml
index c5e2ffac8090528a15668a24c852ec789c1006ab..94af74e7c0e0e5c04c01844572f62389090ddb7c 100644
--- a/src/why3session/why3session_info.ml
+++ b/src/why3session/why3session_info.ml
@@ -15,7 +15,6 @@
 (**************************************************************************)
 
 open Why3
-open Why3session
 open Why3session_lib
 open Whyconf
 open Format
diff --git a/src/why3session/why3session_latex.ml b/src/why3session/why3session_latex.ml
index c2e7ff3590986aaa40ec81b9c11736a5af59b713..27e34f2a70372074260d3af498dc680a2f3d25d3 100644
--- a/src/why3session/why3session_latex.ml
+++ b/src/why3session/why3session_latex.ml
@@ -10,7 +10,6 @@
 (********************************************************************)
 
 open Why3
-open Why3session
 open Why3session_lib
 open Format
 
diff --git a/src/why3session/why3session_lib.ml b/src/why3session/why3session_lib.ml
index ad4105a37e890a7d514683e82139f241c8feb0a5..4c2a69f370270d5ef9303cc98ef0b5363fcde34c 100644
--- a/src/why3session/why3session_lib.ml
+++ b/src/why3session/why3session_lib.ml
@@ -10,7 +10,7 @@
 (********************************************************************)
 
 open Why3
-open Why3session
+
 module S = Session
 module C = Whyconf
 
diff --git a/src/why3session/why3session_lib.mli b/src/why3session/why3session_lib.mli
index bb9902bd7195917ac79480af6ff16079a3b58242..92a8c5156c40246382526099c2d3a1e8ac89d9fb 100644
--- a/src/why3session/why3session_lib.mli
+++ b/src/why3session/why3session_lib.mli
@@ -11,7 +11,6 @@
 
 open Why3
 open Whyconf
-open Why3session
 
 val verbose: Debug.flag
 
diff --git a/src/why3session/why3session_output.ml b/src/why3session/why3session_output.ml
index 87fc9bd7e5b0dc591cda278482cfc5f6a63670f9..cc2e39b5d857db27269473f7b3a88462ddfee9f1 100644
--- a/src/why3session/why3session_output.ml
+++ b/src/why3session/why3session_output.ml
@@ -10,7 +10,6 @@
 (********************************************************************)
 
 open Why3
-open Why3session
 open Why3session_lib
 open Session
 open Format
diff --git a/src/why3session/why3session_rm.ml b/src/why3session/why3session_rm.ml
index 1a57dc73656760e4f3a12cd1464412b2d1473e13..264726087959023967ba6af95e5ea288d0a2d553 100644
--- a/src/why3session/why3session_rm.ml
+++ b/src/why3session/why3session_rm.ml
@@ -10,7 +10,6 @@
 (********************************************************************)
 
 open Why3
-open Why3session
 open Why3session_lib
 open Session
 open Format
diff --git a/src/why3session/why3session_run.ml b/src/why3session/why3session_run.ml
index c9c814a89289d8700375d9817060ec04b778af8e..8b340d7f9b9752b65833640793b0370064316eab 100644
--- a/src/why3session/why3session_run.ml
+++ b/src/why3session/why3session_run.ml
@@ -10,7 +10,6 @@
 (********************************************************************)
 
 open Why3
-open Why3session
 open Why3session_lib
 open Whyconf
 open Session