diff --git a/Makefile.in b/Makefile.in
index f20a23f2216edd774c3c87f77b6dfeba7e88b4b9..70a483db4b669065402aa98f2fe3687b95721ec4 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -59,10 +59,8 @@ OCAMLVERSION = @OCAMLVERSION@
 #PSVIEWER  = @PSVIEWER@
 #PDFVIEWER = @PDFVIEWER@
 
-BFLAGS = -w Ae -dtypes -g -I lib $(INCLUDES)
-OFLAGS = -w Ae -dtypes    -I lib $(INCLUDES)
-DEPFLAGS = -I lib
-
+BFLAGS = -w Ae -dtypes -g -I src $(INCLUDES)
+OFLAGS = -w Ae -dtypes    -I src $(INCLUDES)
 
 # external libraries common to all binaries
 
@@ -84,10 +82,6 @@ all: @OCAMLBEST@
 
 .PHONY: byte opt clean depend all
 
-depend:
-	rm -f $^
-	make $^
-
 #############
 # Why library
 #############
@@ -124,7 +118,7 @@ LIBMODULES = src/config \
 	      $(addprefix src/printer/, $(LIB_PRINTER))
 
 LIBDIRS = util core parser driver transform printer
-LIBINCLUDES = -I src/ $(addprefix -I src/, $(LIBDIRS))
+LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
 
 LIBML  = $(addsuffix .ml,  $(LIBMODULES))
 LIBMLI = $(addsuffix .mli, $(LIBMODULES))
@@ -136,8 +130,8 @@ $(LIBCMX): OFLAGS += -for-pack Why
 
 # build targets
 
-byte: lib/why.cma
-opt:  lib/why.cmxa
+byte: src/why.cma
+opt:  src/why.cmxa
 
 src/why.cma: src/why.cmo
 	$(OCAMLC) -a $(BFLAGS) -o $@ $^
@@ -151,23 +145,12 @@ src/why.cmo: $(LIBCMO)
 src/why.cmx: $(LIBCMX)
 	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
 
-lib/why.cma: src/why.cma
-	cp -f src/why.o lib/why.o
-	cp -f $^ $@
-
-lib/why.cmxa: src/why.cmxa
-	cp -f src/why.a lib/why.a
-	cp -f $^ $@
-
-lib/why.cmi: src/why.cmo src/why.cmx
-	cp -f src/why.cmi lib/why.cmi
-
 # depend target
 
 include .depend.lib
 
 .depend.lib: src/config.ml $(LIBGENERATED)
-	$(OCAMLDEP) $(DEPFLAGS) -slash $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
+	$(OCAMLDEP) -slash -I src $(LIBINCLUDES) $(LIBML) $(LIBMLI) > $@
 
 depend: .depend.lib
 
@@ -191,16 +174,17 @@ clean::
 byte: bin/why.byte
 opt:  bin/why.opt
 
-bin/why.opt: lib/why.cmxa src/main.cmx
+bin/why.opt: src/why.cmxa src/main.cmx
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
 	$(STRIP) $@
 
-bin/why.byte: lib/why.cma src/main.cmo
+bin/why.byte: src/why.cma src/main.cmo
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
 
-src/main.cmo src/main.cmx: lib/why.cmi
+src/main.cmo: src/why.cmo
+src/main.cmx: src/why.cmx
 
 clean::
 	rm -f src/main.cm[iox] src/main.annot src/main.o
@@ -229,12 +213,12 @@ $(PGMCMO) $(PGMCMX): INCLUDES = -I src/programs
 byte: bin/whyml.byte
 opt:  bin/whyml.opt
 
-bin/whyml.opt: lib/why.cmxa $(PGMCMX)
+bin/whyml.opt: src/why.cmxa $(PGMCMX)
 	$(if $(QUIET), @echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
 	$(STRIP) $@
 
-bin/whyml.byte: lib/why.cma $(PGMCMO)
+bin/whyml.byte: src/why.cma $(PGMCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
 
@@ -243,7 +227,7 @@ bin/whyml.byte: lib/why.cma $(PGMCMO)
 include .depend.programs
 
 .depend.programs: $(PGMGENERATED)
-	$(OCAMLDEP) $(DEPFLAGS) -slash -I src/programs $(PGMML) $(PGMMLI) > $@
+	$(OCAMLDEP) -slash -I src -I src/programs $(PGMML) $(PGMMLI) > $@
 
 depend: .depend.programs
 
@@ -274,12 +258,12 @@ opt:  bin/manager.opt
 
 bin/manager.opt bin/manager.byte: INCLUDES = -I +sqlite3
 
-bin/manager.opt: lib/why.cmxa $(MNGCMX)
+bin/manager.opt: src/why.cmxa $(MNGCMX)
 	$(if $(QUIET), @echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) sqlite3.cmxa $^
 	$(STRIP) $@
 
-bin/manager.byte: lib/why.cma $(MNGCMO)
+bin/manager.byte: src/why.cma $(MNGCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) sqlite3.cma $^
 
@@ -288,7 +272,7 @@ bin/manager.byte: lib/why.cma $(MNGCMO)
 include .depend.manager
 
 .depend.manager:
-	$(OCAMLDEP) $(DEPFLAGS) -slash -I src/manager/ $(MNGML) $(MNGMLI) > $@
+	$(OCAMLDEP) -slash -I src -I src/manager $(MNGML) $(MNGMLI) > $@
 
 depend: .depend.manager
 
@@ -322,14 +306,14 @@ endif
 
 bin/whyide.opt bin/whyide.byte: INCLUDES = -I +lablgtk2 -I +threads
 
-bin/whyide.opt: lib/why.cmxa $(IDE_CMX)
+bin/whyide.opt: src/why.cmxa $(IDE_CMX)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
 	    lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^
 	$(STRIP) $@
 
 
-bin/whyide.byte: lib/why.cma $(IDE_CMO)
+bin/whyide.byte: src/why.cma $(IDE_CMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
 	    lablgtk.cma lablgtksourceview2.cma gtkThread.cmo $^
@@ -339,7 +323,7 @@ bin/whyide.byte: lib/why.cma $(IDE_CMO)
 include .depend.ide
 
 .depend.ide:
-	$(OCAMLDEP) $(DEPFLAGS) -slash -I src/ide $(IDEML) $(IDEMLI) > $@
+	$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
 
 depend: .depend.ide
 
@@ -366,7 +350,7 @@ src/coq-plugin/whytac.cmxs: INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES))
 #src/coq-plugin/whytac.cmo:  BFLAGS+=-rectypes
 src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes
 
-src/coq-plugin/whytac.cmxs: lib/why.cmxa src/coq-plugin/whytac.ml
+src/coq-plugin/whytac.cmxs: src/why.cmxa src/coq-plugin/whytac.ml
 	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
 
 #######
@@ -603,8 +587,7 @@ otags:
 wc:
 	ocamlwc -p src/*.ml* src/*/*.ml*
 
-dep:
-	$(MAKE) depend
+dep: depend
 	cat .depend* | ocamldot | dot -Tpdf > dep.pdf
 #	$(PDFVIEWER) dep.pdf
 
@@ -755,6 +738,10 @@ distclean: clean
 	rm -f config.status config.cache config.log \
 	    Makefile src/config.ml doc/version.tex
 
+depend:
+	rm -f $^
+	$(MAKE) $^
+
 #################################################################
 # Building the Why platform with ocamlbuild (OCaml 3.10 needed) #
 #################################################################
diff --git a/src/why.ml b/src/why.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e14a7c4a07952e9e1b2eee2da4f2cd62b8efe5c9
--- /dev/null
+++ b/src/why.ml
@@ -0,0 +1 @@
+(* This file is a stub for ocamldep. Do not delete it. *)