compilation fails with CompCert-3.4 on Linux x86-64; patch proposed

[DAVID MONNIAUX]

> I don't think this is correct, as alloca() may be available even
> though HAVE_ALLOCA is not defined (e.g. with MinGW).
But why would you declare alloca() as a function even though you're not going to use it (as far as I understand you don't use it if HAVE_ALLOCA is not set)?! 

> void *alloca (size_t);
Ok. The following patch also works for CompCert: 
diff -u -r gmp-6.1.2-orig/gmp-impl.h gmp-6.1.2/gmp-impl.h 
--- gmp-6.1.2-orig/gmp-impl.h 2016-12-16 16:45:27.000000000 +0100 
+++ gmp-6.1.2/gmp-impl.h 2019-01-24 15:36:04.121087498 +0100 
@@ -207,7 +207,7 @@ 
# if defined (_AIX) || defined (_IBMR2) 
#pragma alloca 
# else 
- char *alloca (); 
+ void *alloca (size_t); 
# endif 
# endif 
# endif