diff --git a/lib/CoqMakefile.local b/lib/CoqMakefile.local
index d43c3c83f..eacce7b25 100644
--- a/lib/CoqMakefile.local
+++ b/lib/CoqMakefile.local
@@ -4,7 +4,7 @@ CFLAGS=-I$(INCLUDE)
 CC=gcc
 
 proof/math_extern.v: $(SRC)/math_extern.c
-	clightgen -flongdouble -normalize -DCOMPCERT $< -o $@ 
+	clightgen -flongdouble -normalize $< -o $@ 
 
 proof/malloc_extern.v: $(SRC)/malloc_extern.c
 	clightgen -normalize $< -o $@ 
@@ -23,7 +23,7 @@ test/incr.v: test/incr.c
 test/incr_main.v: test/incr_main.c
 	clightgen -I$(INCLUDE) -normalize $<
 test/testmath.v: test/testmath.c
-	clightgen -I$(INCLUDE) -normalize  -DCOMPCERT $<
+	clightgen -I$(INCLUDE) -normalize $<
 
 tests: test/incr
 
diff --git a/lib/proof/src/math_extern.c b/lib/proof/src/math_extern.c
index ec76985e7..3b12d5a13 100644
--- a/lib/proof/src/math_extern.c
+++ b/lib/proof/src/math_extern.c
@@ -1,9 +1,3 @@
-#ifdef COMPCERT
-/* still Starting with CompCert 3.15 (and VST 2.15), don't need this hack
-   any more, but still here for VSTlib compatibility with older versions
-   of CompCert/VST */
-typedef float _Float16;  /* _Float16 is a MacOS thing that CompCert doesn't support */
-#endif
 #include <math.h>
 
 /* Note regard 'long double':
diff --git a/lib/test/testmath.c b/lib/test/testmath.c
index 1022dd5b2..a6ba82491 100644
--- a/lib/test/testmath.c
+++ b/lib/test/testmath.c
@@ -1,9 +1,3 @@
-#ifdef COMPCERT
-/* still Starting with CompCert 3.15 (and VST 2.15), don't need this hack
-   any more, but still here for VSTlib compatibility with older versions
-   of CompCert/VST */
-typedef float _Float16;  /* _Float16 is a MacOS thing that CompCert doesn't support */
-#endif
 #include <math.h>
 
 double f(double t) {