diff --git a/.gitignore b/.gitignore
index e825853e38c9a8663b97a4517b3dea128c03cc1d..a0e1423832ff019d183fba1a156584ba6d617b2a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -148,8 +148,7 @@ why3.conf
 /share/emacs/semantic.cache
 /share/Makefile.config
 /share/drivers
-/share/modules
-/share/theories
+/share/stdlib
 
 # /src/
 /src/config.sh
@@ -301,15 +300,6 @@ pvsbin/
 /examples/prover/bench1
 /examples/prover/bench2
 
-# modules
-/modules/string/
-/modules/stack/
-/modules/queue/
-/modules/pqueue/
-/modules/mach/array/
-/modules/mach/int/
-/modules/python/
-
 # Try Why3
 /src/trywhy3/trywhy3.byte
 /src/trywhy3/trywhy3.js
diff --git a/Makefile.in b/Makefile.in
index 72533db153ce2513a3b906f75a322ab740528405..5a30226b57fca5fb06467f319a259b5699180cc0 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -315,12 +315,11 @@ install_no_local::
 	$(MKDIR_P) $(DATADIR)/why3/vim/ftdetect
 	$(MKDIR_P) $(DATADIR)/why3/vim/syntax
 	$(MKDIR_P) $(DATADIR)/why3/lang
-	$(MKDIR_P) $(DATADIR)/why3/theories
-	$(MKDIR_P) $(DATADIR)/why3/modules/mach
+	$(MKDIR_P) $(DATADIR)/why3/stdlib
+	$(MKDIR_P) $(DATADIR)/why3/stdlib/mach
 	$(MKDIR_P) $(DATADIR)/why3/drivers
-	$(INSTALL_DATA) theories/*.why $(DATADIR)/why3/theories
-	$(INSTALL_DATA) modules/*.mlw $(DATADIR)/why3/modules
-	$(INSTALL_DATA) modules/mach/*.mlw $(DATADIR)/why3/modules/mach
+	$(INSTALL_DATA) stdlib/*.why stdlib/*.mlw $(DATADIR)/why3/stdlib
+	$(INSTALL_DATA) stdlib/mach/*.mlw $(DATADIR)/why3/stdlib/mach
 	$(INSTALL_DATA) drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
 	$(INSTALL_DATA) LICENSE $(DATADIR)/why3/
 	$(INSTALL_DATA) share/provers-detection-data.conf $(DATADIR)/why3/
@@ -563,16 +562,13 @@ install_local:: bin/why3 $(addprefix bin/,$(TOOLS_BIN))
 bin/%:	bin/%.@OCAMLBEST@
 	ln -sf $(notdir $<) $@
 
-install_local:: share/drivers share/modules share/theories
+install_local:: share/drivers share/stdlib
 
 share/drivers:
 	ln -snf ../drivers share/drivers
 
-share/modules:
-	ln -snf ../modules share/modules
-
-share/theories:
-	ln -snf ../theories share/theories
+share/stdlib:
+	ln -snf ../stdlib share/stdlib
 
 ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
 -include $(TOOLSDEP)
@@ -677,7 +673,7 @@ gallery-subs::
 	  echo "exporting examples/$$d"; \
 	  mkdir -p $(GALLERYDIR)/$$d; \
 	  cd examples/$$d; \
-	  WHY3CONFIG="" ../../bin/why3doc.@OCAMLBEST@ -L ../../theories -L ../../modules -L . --stdlib-url http://why3.lri.fr/stdlib/ *.mlw -o $(GALLERYDIR)/$$d; \
+	  WHY3CONFIG="" ../../bin/why3doc.@OCAMLBEST@ -L ../../stdlib -L . --stdlib-url http://why3.lri.fr/stdlib/ *.mlw -o $(GALLERYDIR)/$$d; \
 	  cd ..; \
 	  rm -f $(GALLERYDIR)/$$d/$$d.zip; \
 	  zip -q -r $(GALLERYDIR)/$$d/$$d.zip $$d; \
@@ -1095,41 +1091,41 @@ drivers/coq-realizations.aux: Makefile
 
 update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float
 
-update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
-	for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o $(GENERATED_PREFIX_COQ)/int/; done
+update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/int.why
+	for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T int.$$f -o $(GENERATED_PREFIX_COQ)/int/; done
 
-update-coq-bool: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bool.why
-	for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bool.$$f -o $(GENERATED_PREFIX_COQ)/bool/; done
+update-coq-bool: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/bool.why
+	for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T bool.$$f -o $(GENERATED_PREFIX_COQ)/bool/; done
 
-update-coq-real: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/real.why
-	for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T real.$$f -o $(GENERATED_PREFIX_COQ)/real/; done
+update-coq-real: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/real.why
+	for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T real.$$f -o $(GENERATED_PREFIX_COQ)/real/; done
 
-update-coq-number: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/number.why
-	for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T number.$$f -o $(GENERATED_PREFIX_COQ)/number/; done
+update-coq-number: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/number.why
+	for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T number.$$f -o $(GENERATED_PREFIX_COQ)/number/; done
 
-update-coq-set: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/set.why
-	for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T set.$$f -o $(GENERATED_PREFIX_COQ)/set/; done
+update-coq-set: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/set.why
+	for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T set.$$f -o $(GENERATED_PREFIX_COQ)/set/; done
 
-update-coq-map: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/map.why
-	for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T map.$$f -o $(GENERATED_PREFIX_COQ)/map/; done
+update-coq-map: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/map.why
+	for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T map.$$f -o $(GENERATED_PREFIX_COQ)/map/; done
 
-update-coq-list: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/list.why
-	for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T list.$$f -o $(GENERATED_PREFIX_COQ)/list/; done
+update-coq-list: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/list.why
+	for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T list.$$f -o $(GENERATED_PREFIX_COQ)/list/; done
 
-update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/option.why
-	for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T option.$$f -o $(GENERATED_PREFIX_COQ)/option/; done
+update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/option.why
+	for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T option.$$f -o $(GENERATED_PREFIX_COQ)/option/; done
 
-update-coq-seq: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/seq.why
-	for f in $(COQLIBS_SEQ_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T seq.$$f -o $(GENERATED_PREFIX_COQ)/seq/; done
+update-coq-seq: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/seq.why
+	for f in $(COQLIBS_SEQ_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T seq.$$f -o $(GENERATED_PREFIX_COQ)/seq/; done
 
-update-coq-bv: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bv.why
-	for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bv.$$f -o $(GENERATED_PREFIX_COQ)/bv/; done
+update-coq-bv: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/bv.why
+	for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T bv.$$f -o $(GENERATED_PREFIX_COQ)/bv/; done
 
-update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/ieee_float.why
-	for f in $(COQLIBS_IEEEFLOAT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T ieee_float.$$f -o $(GENERATED_PREFIX_COQ)/ieee_float/; done
+update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/ieee_float.why
+	for f in $(COQLIBS_IEEEFLOAT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T ieee_float.$$f -o $(GENERATED_PREFIX_COQ)/ieee_float/; done
 
-update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/floating_point.why
-	for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o $(GENERATED_PREFIX_COQ)/floating_point/; done
+update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/floating_point.why
+	for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T floating_point.$$f -o $(GENERATED_PREFIX_COQ)/floating_point/; done
 
 
 ifeq (@enable_coq_support@,yes)
@@ -1260,11 +1256,11 @@ install_no_local::
 	$(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
 
 update-pvs: bin/why3realize.@OCAMLBEST@ drivers/pvs-realizations.aux
-	for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
-	for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
-	for f in $(PVSLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; done
-	for f in $(PVSLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; done
-	for f in $(PVSLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T floating_point.$$f -o lib/pvs/floating_point/; done
+	for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
+	for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
+	for f in $(PVSLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; done
+	for f in $(PVSLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; done
+	for f in $(PVSLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T floating_point.$$f -o lib/pvs/floating_point/; done
 
 else
 
@@ -1359,58 +1355,58 @@ endif
 update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
 
 $(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
-  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/int.why
+  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/int.why
 	$(SHOW) "Generating Isabelle realization for int.$(notdir $(basename $@))"
 	$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/int
-	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/int/
+	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/int/
 
 $(ISABELLELIBS_BOOL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
-  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bool.why
+  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/bool.why
 	$(SHOW) "Generating Isabelle realization for bool.$(notdir $(basename $@))"
 	$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/bool
-	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bool/
+	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bool/
 
 $(ISABELLELIBS_REAL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
-  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/real.why
+  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/real.why
 	$(SHOW) "Generating Isabelle realization for real.$(notdir $(basename $@))"
 	$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/real
-	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/real/
+	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/real/
 
 $(ISABELLELIBS_NUMBER): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
-  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/number.why
+  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/number.why
 	$(SHOW) "Generating Isabelle realization for number.$(notdir $(basename $@))"
 	$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/number
-	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/number/
+	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/number/
 
 $(ISABELLELIBS_SET): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
-  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/set.why
+  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/set.why
 	$(SHOW) "Generating Isabelle realization for set.$(notdir $(basename $@))"
 	$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/set
-	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/set/
+	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/set/
 
 $(ISABELLELIBS_MAP): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
-  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/map.why
+  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/map.why
 	$(SHOW) "Generating Isabelle realization for map.$(notdir $(basename $@))"
 	$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/map
-	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/map/
+	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/map/
 
 $(ISABELLELIBS_LIST): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
-  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/list.why
+  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/list.why
 	$(SHOW) "Generating Isabelle realization for list.$(notdir $(basename $@))"
 	$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/list
-	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/list/
+	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/list/
 
 $(ISABELLELIBS_OPTION): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
-  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/option.why
+  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/option.why
 	$(SHOW) "Generating Isabelle realization for option.$(notdir $(basename $@))"
 	$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/option
-	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/option/
+	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/option/
 
 $(ISABELLELIBS_BV): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
-  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bv.why
+  $(ISABELLEREALIZEDRV) drivers/isabelle-common.gen stdlib/bv.why
 	$(SHOW) "Generating Isabelle realization for bv.$(notdir $(basename $@))"
 	$(HIDE)mkdir -p $(GENERATED_PREFIX_ISABELLE)/bv
-	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bv/
+	$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bv/
 
 $(GENERATED_PREFIX_ISABELLE)/last_build: $(ISABELLEVERSIONSPECIFICTARGETS)
 # $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
@@ -1668,7 +1664,7 @@ src/trywhy3/trywhy3.byte: src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo
 src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte
 	js_of_ocaml $(JSOO_DEBUG) --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
 		--file=try_alt_ergo.drv:/ \
-		`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/%p"` \
+		`find stdlib \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/%p"` \
 	+weak.js +nat.js $<
 
 src/trywhy3/why3_worker.byte: $(TRYWHY3CMO) src/trywhy3/worker_proto.cmo src/trywhy3/why3_worker.cmo
@@ -1966,59 +1962,55 @@ install_no_local::
 
 .PHONY: stdlibdoc
 
-STDLIBS = algebra \
-	bag \
-	bintree \
-	bool \
-	bv \
-	floating_point \
-	graph \
-	int \
-	ieee_float \
-	list \
-	map \
-	number \
-	option \
-	pigeon \
-	real \
-	relations \
-	seq \
-	set \
-	sum
+STDLIBS = \
+	algebra.why \
+	array.mlw \
+	bag.why \
+	bintree.why \
+	bool.why \
+	bv.why \
+	floating_point.why \
+	graph.why \
+	hashtbl.mlw \
+	impset.mlw \
+	int.why \
+	ieee_float.why \
+	list.why \
+	map.why \
+	matrix.mlw \
+	number.why \
+	option.why \
+	pigeon.why \
+	pqueue.mlw \
+	queue.mlw \
+	random.mlw \
+	real.why \
+	ref.mlw \
+	relations.why \
+	seq.why \
+	set.why \
+	stack.mlw \
+	string.mlw \
+	sum.why \
+	mach/array.mlw \
+	mach/int.mlw
 # function ? tptp ?
 
-STDMODS = array \
-	hashtbl \
-	impset \
-	matrix \
-	pqueue \
-	queue \
-	random \
-	ref \
-	stack \
-	string
-
-STDMACS = array int
-
-STDLIBFILES = $(addsuffix .why, $(addprefix theories/, $(STDLIBS)))
-STDMODFILES = $(addsuffix .mlw, $(addprefix modules/, $(STDMODS)))
-STDMACFILES = $(addsuffix .mlw, $(addprefix modules/mach/, $(STDMACS)))
+STDLIBFILES = $(addprefix stdlib/, $(STDLIBS))
 
 # TODO: remove the hack about int.why once it has become builtin
-stdlibdoc: $(STDLIBFILES) $(STDMODFILES) bin/why3doc.@OCAMLBEST@
+stdlibdoc: $(STDLIBFILES) bin/why3doc.@OCAMLBEST@
 	mkdir -p doc/stdlibdoc
-	sed -e "s/use import Int/use import int.Int/" theories/int.why > int.why
+	sed -e "s/use import Int/use import int.Int/" stdlib/int.why > int.why
 	rm -f doc/stdlibdoc/style.css
-	WHY3CONFIG="" bin/why3doc.@OCAMLBEST@ -L theories -L modules \
+	WHY3CONFIG="" bin/why3doc.@OCAMLBEST@ -L stdlib \
           -o doc/stdlibdoc --title "Why3 Standard Library" \
-	  $(subst theories/int.why,int.why,$(STDLIBFILES)) $(STDMODFILES) $(STDMACFILES)
+	  $(subst stdlib/int.why,int.why,$(STDLIBFILES))
 	rm int.why
 	cd doc/stdlibdoc; \
-	  for f in theories.*.html; \
-	    do mv "$$f" "$${f#theories.}"; done; \
-	  for f in modules.*.html; \
-	    do mv "$$f" "$${f#modules.}"; done
-	sed -i -e "s#theories.##g" -e "s#modules.##g" doc/stdlibdoc/index.html
+	  for f in stdlib.*.html; \
+	    do mv "$$f" "$${f#stdlib.}"; done
+	sed -i -e "s#stdlib.##g" doc/stdlibdoc/index.html
 	sed -i -e "s#int\.\(<a href=\"int\.html\)#\1#g" doc/stdlibdoc/int.html
 
 clean::
diff --git a/README.md b/README.md
index d9bbd59792da9b6a2575c3692ae29ca172a94d54..22a083bc23130a48be3cfbd22ebbe094a73bbe3e 100644
--- a/README.md
+++ b/README.md
@@ -26,7 +26,7 @@ The documentation (a tutorial and a reference manual) is in the file
 [doc/manual.pdf](http://why3.lri.fr/manual.pdf) or online at
 http://why3.lri.fr/doc/.
 
-Various examples can be found in the subdirectories [theories/](theories)
+Various examples can be found in the subdirectories [stdlib/](stdlib)
 and [examples/](examples).
 
 Mailing list (Why3 Club):
diff --git a/bench/bench b/bench/bench
index c04338304c50ea64f35edd9613b34360af9a269b..5f52d0b74fbf17a0153769022c7ce6f09f665984 100755
--- a/bench/bench
+++ b/bench/bench
@@ -1,4 +1,3 @@
-
 #!/bin/bash
 
 # auto bench for why
@@ -10,17 +9,20 @@
 
 suffix=$1
 
+# TODO: remove the hack about int.why once it has become builtin
 goods () {
     pgm="bin/why3prove$suffix"
     ERROR=
     rm -f bench_errors
     for f in $1/*.[wm][hl][yw] ; do
 	printf "  $f... "
+        opts="$2"
+        if test $f = stdlib/int.why; then opts="$2 --type-only"; fi
 	# running Why
-	if ! $pgm $2 $f > /dev/null 2> bench_error; then
+	if ! $pgm $opts $f > /dev/null 2> bench_error; then
 	    echo "FAILED!"
 #            echo "env: WHY3DATA='$WHY3DATA'"
-            echo "invocation: $pgm $2 $f" | tee -a bench_errors
+            echo "invocation: $pgm $opts $f" | tee -a bench_errors
             cat bench_error | tee -a bench_errors
             ERROR=yes
 	elif test -s bench_error; then
@@ -174,13 +176,9 @@ list_stuff () {
     fi
 }
 
-echo "=== Checking theories ==="
-goods theories --type-only # FIXME remove --type-only
-echo ""
-
-echo "=== Checking modules ==="
-goods modules
-goods modules/mach
+echo "=== Checking stdlib ==="
+goods stdlib
+goods stdlib/mach
 echo ""
 
 echo "=== Checking drivers ==="
diff --git a/bench/encoding/why.conf b/bench/encoding/why.conf
index e3d45bdeecc2333590d305d8dcdc5e2aea09f400..5525a78ff5b84d16784f5fef01d31d9eab50ad65 100644
--- a/bench/encoding/why.conf
+++ b/bench/encoding/why.conf
@@ -1,5 +1,5 @@
-[main ]
-loadpath = "../../share/theories"
+[main]
+loadpath = "../../share/stdlib"
 magic = 5
 memlimit = 2048
 running_provers_max = 7
diff --git a/examples/stdlib/array/why3session.xml b/examples/stdlib/array/why3session.xml
index 6ca9cc7f8e6818586812b90f4e207e605b2ad833..47f226edcc87c80456fcaa0b687b0dfc889aad54 100644
--- a/examples/stdlib/array/why3session.xml
+++ b/examples/stdlib/array/why3session.xml
@@ -8,7 +8,7 @@
 <prover id="3" name="Coq" version="8.6.1" timelimit="6" steplimit="0" memlimit="1000"/>
 <prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../../../modules/array.mlw" proved="true">
+<file name="../../../stdlib/array.mlw" proved="true">
 <theory name="Array" proved="true" sum="d12f98c64e888261d80af67de4830724">
  <goal name="VC array" expl="VC for array" proved="true">
  <proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
diff --git a/examples/stdlib/bintree/why3session.xml b/examples/stdlib/bintree/why3session.xml
index 19d1c1abe8d856ee44325384085b5b43b30f4f11..26a175cb493f718a07f8bd504baf4da764f358d5 100644
--- a/examples/stdlib/bintree/why3session.xml
+++ b/examples/stdlib/bintree/why3session.xml
@@ -4,7 +4,7 @@
 <why3session shape_version="4">
 <prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
-<file name="../../../theories/bintree.why" expanded="true">
+<file name="../../../stdlib/bintree.why" expanded="true">
 <theory name="Tree" sum="c05a159c0fca07eac9e3cabdb81061c8">
  <goal name="VC is_empty" expl="VC for is_empty">
  <transf name="split_goal_wp">
diff --git a/examples/stdlib/list/why3session.xml b/examples/stdlib/list/why3session.xml
index 132cce40b869133d41ef6aea19dd38fa1a7b0699..6d4dcf8e049b62efd06912601955d57910f9cae6 100644
--- a/examples/stdlib/list/why3session.xml
+++ b/examples/stdlib/list/why3session.xml
@@ -7,7 +7,7 @@
 <prover id="3" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../../../theories/list.why" expanded="true">
+<file name="../../../stdlib/list.why" expanded="true">
 <theory name="List" sum="0837e0e504ae2d2a2dc07ff388fab3e5">
  <goal name="VC is_nil" expl="VC for is_nil">
  <proof prover="6"><result status="valid" time="0.00" steps="7"/></proof>
diff --git a/src/driver/whyconf.ml b/src/driver/whyconf.ml
index 984a473a7cb393983f3abea1e2c8fc36822317b2..9a11626622e9001cbddc6233b3260a22a47de618 100644
--- a/src/driver/whyconf.ml
+++ b/src/driver/whyconf.ml
@@ -42,8 +42,7 @@ let why3_regexp_of_string s = (* define a regexp in why3 *)
 (* lib and shared dirs *)
 
 let default_loadpath =
-  [ Filename.concat Config.datadir "theories";
-    Filename.concat Config.datadir "modules"; ]
+  [ Filename.concat Config.datadir "stdlib" ]
 
 let default_conf_file =
   match Config.localdir with
@@ -184,7 +183,7 @@ let set_strategies rc strategies =
 type main = {
   libdir   : string;      (* "/usr/local/lib/why/" *)
   datadir  : string;      (* "/usr/local/share/why/" *)
-  loadpath  : string list;  (* "/usr/local/lib/why/theories" *)
+  loadpath  : string list;  (* "/usr/local/lib/why/stdlib" *)
   timelimit : int;
   (* default prover time limit in seconds (0 unlimited) *)
   memlimit  : int;
diff --git a/src/trywhy3/trywhy3.conf b/src/trywhy3/trywhy3.conf
index 80b07cf1193125c80e0d52b8e23e605a40ae2cae..b4e65e018edc744d6341c6e0dfdc1e9ca532eee9 100644
--- a/src/trywhy3/trywhy3.conf
+++ b/src/trywhy3/trywhy3.conf
@@ -1,7 +1,6 @@
 [main]
 cntexample = false
-loadpath = "/theories"
-loadpath = "/modules"
+loadpath = "/stdlib"
 magic = 14
 memlimit = 1000
 running_provers_max = 2
diff --git a/theories/algebra.why b/stdlib/algebra.why
similarity index 100%
rename from theories/algebra.why
rename to stdlib/algebra.why
diff --git a/modules/appmap.mlw b/stdlib/appmap.mlw
similarity index 100%
rename from modules/appmap.mlw
rename to stdlib/appmap.mlw
diff --git a/modules/appset.mlw b/stdlib/appset.mlw
similarity index 100%
rename from modules/appset.mlw
rename to stdlib/appset.mlw
diff --git a/modules/array.mlw b/stdlib/array.mlw
similarity index 100%
rename from modules/array.mlw
rename to stdlib/array.mlw
diff --git a/theories/bag.why b/stdlib/bag.why
similarity index 100%
rename from theories/bag.why
rename to stdlib/bag.why
diff --git a/theories/bintree.why b/stdlib/bintree.why
similarity index 100%
rename from theories/bintree.why
rename to stdlib/bintree.why
diff --git a/theories/bool.why b/stdlib/bool.why
similarity index 100%
rename from theories/bool.why
rename to stdlib/bool.why
diff --git a/theories/bv.why b/stdlib/bv.why
similarity index 100%
rename from theories/bv.why
rename to stdlib/bv.why
diff --git a/modules/cursor.mlw b/stdlib/cursor.mlw
similarity index 100%
rename from modules/cursor.mlw
rename to stdlib/cursor.mlw
diff --git a/modules/exn.mlw b/stdlib/exn.mlw
similarity index 100%
rename from modules/exn.mlw
rename to stdlib/exn.mlw
diff --git a/theories/floating_point.why b/stdlib/floating_point.why
similarity index 100%
rename from theories/floating_point.why
rename to stdlib/floating_point.why
diff --git a/theories/function.why b/stdlib/function.why
similarity index 100%
rename from theories/function.why
rename to stdlib/function.why
diff --git a/theories/graph.why b/stdlib/graph.why
similarity index 100%
rename from theories/graph.why
rename to stdlib/graph.why
diff --git a/modules/hashtbl.mlw b/stdlib/hashtbl.mlw
similarity index 100%
rename from modules/hashtbl.mlw
rename to stdlib/hashtbl.mlw
diff --git a/theories/ieee_float.why b/stdlib/ieee_float.why
similarity index 100%
rename from theories/ieee_float.why
rename to stdlib/ieee_float.why
diff --git a/modules/impmap.mlw b/stdlib/impmap.mlw
similarity index 100%
rename from modules/impmap.mlw
rename to stdlib/impmap.mlw
diff --git a/modules/impset.mlw b/stdlib/impset.mlw
similarity index 100%
rename from modules/impset.mlw
rename to stdlib/impset.mlw
diff --git a/theories/int.why b/stdlib/int.why
similarity index 100%
rename from theories/int.why
rename to stdlib/int.why
diff --git a/modules/io.mlw b/stdlib/io.mlw
similarity index 100%
rename from modules/io.mlw
rename to stdlib/io.mlw
diff --git a/theories/list.why b/stdlib/list.why
similarity index 100%
rename from theories/list.why
rename to stdlib/list.why
diff --git a/modules/mach/array.mlw b/stdlib/mach/array.mlw
similarity index 100%
rename from modules/mach/array.mlw
rename to stdlib/mach/array.mlw
diff --git a/modules/mach/bv.mlw b/stdlib/mach/bv.mlw
similarity index 100%
rename from modules/mach/bv.mlw
rename to stdlib/mach/bv.mlw
diff --git a/modules/mach/float.mlw b/stdlib/mach/float.mlw
similarity index 100%
rename from modules/mach/float.mlw
rename to stdlib/mach/float.mlw
diff --git a/modules/mach/int.mlw b/stdlib/mach/int.mlw
similarity index 100%
rename from modules/mach/int.mlw
rename to stdlib/mach/int.mlw
diff --git a/modules/mach/matrix.mlw b/stdlib/mach/matrix.mlw
similarity index 100%
rename from modules/mach/matrix.mlw
rename to stdlib/mach/matrix.mlw
diff --git a/modules/mach/onetime.mlw b/stdlib/mach/onetime.mlw
similarity index 100%
rename from modules/mach/onetime.mlw
rename to stdlib/mach/onetime.mlw
diff --git a/modules/mach/peano.mlw b/stdlib/mach/peano.mlw
similarity index 100%
rename from modules/mach/peano.mlw
rename to stdlib/mach/peano.mlw
diff --git a/theories/map.why b/stdlib/map.why
similarity index 100%
rename from theories/map.why
rename to stdlib/map.why
diff --git a/modules/matrix.mlw b/stdlib/matrix.mlw
similarity index 100%
rename from modules/matrix.mlw
rename to stdlib/matrix.mlw
diff --git a/modules/null.mlw b/stdlib/null.mlw
similarity index 100%
rename from modules/null.mlw
rename to stdlib/null.mlw
diff --git a/theories/number.why b/stdlib/number.why
similarity index 100%
rename from theories/number.why
rename to stdlib/number.why
diff --git a/modules/ocaml.mlw b/stdlib/ocaml.mlw
similarity index 100%
rename from modules/ocaml.mlw
rename to stdlib/ocaml.mlw
diff --git a/theories/option.why b/stdlib/option.why
similarity index 100%
rename from theories/option.why
rename to stdlib/option.why
diff --git a/theories/pigeon.why b/stdlib/pigeon.why
similarity index 100%
rename from theories/pigeon.why
rename to stdlib/pigeon.why
diff --git a/modules/pqueue.mlw b/stdlib/pqueue.mlw
similarity index 100%
rename from modules/pqueue.mlw
rename to stdlib/pqueue.mlw
diff --git a/modules/python.mlw b/stdlib/python.mlw
similarity index 100%
rename from modules/python.mlw
rename to stdlib/python.mlw
diff --git a/modules/queue.mlw b/stdlib/queue.mlw
similarity index 100%
rename from modules/queue.mlw
rename to stdlib/queue.mlw
diff --git a/modules/random.mlw b/stdlib/random.mlw
similarity index 100%
rename from modules/random.mlw
rename to stdlib/random.mlw
diff --git a/theories/real.why b/stdlib/real.why
similarity index 100%
rename from theories/real.why
rename to stdlib/real.why
diff --git a/modules/ref.mlw b/stdlib/ref.mlw
similarity index 100%
rename from modules/ref.mlw
rename to stdlib/ref.mlw
diff --git a/theories/regexp.why b/stdlib/regexp.why
similarity index 100%
rename from theories/regexp.why
rename to stdlib/regexp.why
diff --git a/theories/relations.why b/stdlib/relations.why
similarity index 100%
rename from theories/relations.why
rename to stdlib/relations.why
diff --git a/theories/seq.why b/stdlib/seq.why
similarity index 100%
rename from theories/seq.why
rename to stdlib/seq.why
diff --git a/theories/set.why b/stdlib/set.why
similarity index 100%
rename from theories/set.why
rename to stdlib/set.why
diff --git a/modules/stack.mlw b/stdlib/stack.mlw
similarity index 100%
rename from modules/stack.mlw
rename to stdlib/stack.mlw
diff --git a/modules/string.mlw b/stdlib/string.mlw
similarity index 100%
rename from modules/string.mlw
rename to stdlib/string.mlw
diff --git a/theories/sum.why b/stdlib/sum.why
similarity index 100%
rename from theories/sum.why
rename to stdlib/sum.why
diff --git a/theories/tptp.why b/stdlib/tptp.why
similarity index 100%
rename from theories/tptp.why
rename to stdlib/tptp.why
diff --git a/theories/tree.why b/stdlib/tree.why
similarity index 100%
rename from theories/tree.why
rename to stdlib/tree.why