diff --git a/lib/CoqMakefile.local b/lib/CoqMakefile.local
index eacce7b25..d43c3c83f 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 $< -o $@ 
+	clightgen -flongdouble -normalize -DCOMPCERT $< -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 $<
+	clightgen -I$(INCLUDE) -normalize  -DCOMPCERT $<
 
 tests: test/incr
 
diff --git a/lib/proof/src/math_extern.c b/lib/proof/src/math_extern.c
index 3b12d5a13..0a17ead09 100644
--- a/lib/proof/src/math_extern.c
+++ b/lib/proof/src/math_extern.c
@@ -1,3 +1,6 @@
+#ifdef COMPCERT
+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 a6ba82491..cb1ea957c 100644
--- a/lib/test/testmath.c
+++ b/lib/test/testmath.c
@@ -1,3 +1,6 @@
+#ifdef COMPCERT
+typedef float _Float16;  /* _Float16 is a MacOS thing that CompCert doesn't support */
+#endif
 #include <math.h>
 
 double f(double t) {