diff --git a/src/Appli/Axpy.v b/src/Appli/Fappli_Axpy.v
similarity index 98%
rename from src/Appli/Axpy.v
rename to src/Appli/Fappli_Axpy.v
index b1ff17d7de3148855776f3784f50e84a63fce606..9a575e49a228820370e76f5954aebaa6788c579d 100644
--- a/src/Appli/Axpy.v
+++ b/src/Appli/Fappli_Axpy.v
@@ -35,3 +35,6 @@ Theorem Axpy_opt :
       bpow (1-prec) / (6*bpow 1) * Rabs y)%R ->
          (MinOrMax (a1 * x1 + y1) u).
 Admitted.
+
+
+End Axpy.
\ No newline at end of file
diff --git a/src/Makefile.am b/src/Makefile.am
index 627b001f05d09386a6144fc311eb79fc9ffad63d..f2795a95f970d7aa2191343e7318d2c008f63513 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -22,7 +22,8 @@ FILES = \
 	Prop/Fprop_plus_error.v \
 	Prop/Fprop_relative.v \
 	Prop/Fprop_div_sqrt_error.v \
-	Prop/Fprop_Sterbenz.v
+	Prop/Fprop_Sterbenz.v \
+	Appli/Fappli_Axpy.v
 
 EXTRA_DIST = $(FILES)
 CLEANFILES = $(FILES:=o) $(FILES:=d) $(FILES:.v=.glob)