diff --git a/common/Why3__BuiltIn.ml b/common/Why3__BuiltIn.ml
new file mode 100644
index 0000000000000000000000000000000000000000..49b4392a60a8f74a198686acda631f2d2119c8e5
--- /dev/null
+++ b/common/Why3__BuiltIn.ml
@@ -0,0 +1 @@
+type real = unit