diff --git a/Makefile.am b/Makefile.am
index a5a85ae2e09ab277175d07e2b8e7e7c29a484b27..9ce812d552989e7a09b777ebe711d2f8ad910bb4 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -1,20 +1,2 @@
-FILES = \
-	Flocq_Raux.v \
-	Flocq_defs.v \
-	Flocq_rnd_ex.v
-
-data_DATA = $(FILES:=o)
-EXTRA_DIST = autogen.sh $(FILES)
-CLEANFILES = $(FILES:=o) $(FILES:=d)
-
-datadir = $(libdir)
-
-%.vo: %.v
-	@echo COQC $<
-	@$(COQC) $(COQRFLAG) $<
-
-%.vd: %.v
-	@echo COQDEP $<
-	@$(COQDEP) $< | sed -e 's,\($*\)\.vo[ :]*,\1.vo $@ : ,g' > $@
-
-include $(FILES:=d)
+SUBDIRS = src
+EXTRA_DIST = autogen.sh
diff --git a/configure.ac b/configure.ac
index 6de53cb56ae67cbdcd585f8b1077545cab076cad..ce0c27ec81b6d7eed20026a2b4bb6ba84f5331b3 100644
--- a/configure.ac
+++ b/configure.ac
@@ -28,5 +28,5 @@ AC_SUBST(COQRFLAG, ['-R . Flocq'])
 AC_ARG_ENABLE([prefix], AS_HELP_STRING([--disable-prefix], [do not compile files into a Flocq module]),
   [if test "$enable_prefix" = "no"; then COQRFLAG= ; fi], [])
 
-AC_CONFIG_FILES([Makefile])
+AC_CONFIG_FILES([Makefile src/Makefile])
 AC_OUTPUT
diff --git a/Flocq_Raux.v b/src/Flocq_Raux.v
similarity index 100%
rename from Flocq_Raux.v
rename to src/Flocq_Raux.v
diff --git a/Flocq_defs.v b/src/Flocq_defs.v
similarity index 100%
rename from Flocq_defs.v
rename to src/Flocq_defs.v
diff --git a/Flocq_rnd_ex.v b/src/Flocq_rnd_ex.v
similarity index 99%
rename from Flocq_rnd_ex.v
rename to src/Flocq_rnd_ex.v
index 139d813e71e8eff695e078848887c79c0c6ae211..d45feecffc8fd64f6b04828d7c3d5d19e007bb93 100644
--- a/Flocq_rnd_ex.v
+++ b/src/Flocq_rnd_ex.v
@@ -230,6 +230,7 @@ now apply H2.
 now apply Ropp_le_contravar.
 Qed.
 
+(*
 Theorem satisfies_any_imp_ZR: forall (F:R->Prop),
    satisfies_any F ->
        exists rnd:R-> R, Rnd_ZR R_whole F rnd.
@@ -241,7 +242,7 @@ exists (fun x =>  match Rle_dec 0 x with
 split ; intros x (_, Hx).
 (* rnd DN *)
 destruct (Rle_dec 0 x) as [_|H'].
-apply H3.
+now apply H3.
 elim (H' Hx).
 (* rnd UP *)
 destruct (Rle_dec 0 x) as [H'|H'].
@@ -757,5 +758,6 @@ intros.
 apply Rnd_DN_is_rounding.
 eapply FIX_format_satisfies_DN_UP.
 Qed.
+*)
 
-End RND.
\ No newline at end of file
+End RND_ex.
\ No newline at end of file
diff --git a/src/Makefile.am b/src/Makefile.am
new file mode 100644
index 0000000000000000000000000000000000000000..08bf8493e897781c217f2d3b8f28b149078bbba3
--- /dev/null
+++ b/src/Makefile.am
@@ -0,0 +1,20 @@
+FILES = \
+	Flocq_Raux.v \
+	Flocq_defs.v \
+	Flocq_rnd_ex.v
+
+data_DATA = $(FILES:=o)
+EXTRA_DIST = $(FILES)
+CLEANFILES = $(FILES:=o) $(FILES:=d)
+
+datadir = $(libdir)
+
+%.vo: %.v
+	@echo COQC $<
+	@$(COQC) $(COQRFLAG) $<
+
+%.vd: %.v
+	@echo COQDEP $<
+	@$(COQDEP) $< > $@
+
+-include $(FILES:=d)