diff --git a/.gitignore b/.gitignore
index 664bfb8a35991957c996ca70113c2971f9ab1645..3f6a86c1ce038a709fce36c04169c483ac20def7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -15,3 +15,16 @@ why3shapes.gz
 # dependencies (remove it later & use submodules instead ?)
 dolmen/
 farith/
+
+# coq artifacts
+
+**/*.vo
+**/*.vok
+**/*.glob
+**/*.lia.cache
+**/*.aux
+**/*.vk
+**/.CoqMakefile.d
+**/*.vos
+**/CoqMakefile
+**/CoqMakefile.conf
diff --git a/src_common/ieee/coq/Fauto.v b/src_common/ieee/coq/Fauto.v
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src_common/ieee/coq/Futils.v b/src_common/ieee/coq/Futils.v
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src_common/ieee/coq/Makefile b/src_common/ieee/coq/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..5d5d859342cfb12495077c082965edf1c6f21695
--- /dev/null
+++ b/src_common/ieee/coq/Makefile
@@ -0,0 +1,4 @@
+include CoqMakefile
+
+CoqMakefile:
+	coq_makefile -f _CoqProject -o CoqMakefile
\ No newline at end of file
diff --git a/src_common/ieee/coq/_CoqProject b/src_common/ieee/coq/_CoqProject
new file mode 100644
index 0000000000000000000000000000000000000000..02869ee062dd5d81e7d1615eadd205e55c82c79a
--- /dev/null
+++ b/src_common/ieee/coq/_CoqProject
@@ -0,0 +1,4 @@
+-R ./ Finterval
+./Finterval.v
+./Fauto.v
+./Futils.v
\ No newline at end of file