Rely on ocamlc to call the C compiler...

...with proper options for dynamic loading of C stubs. I believe this
is the preferred way of compiling C stubs. It also adds by itself
-fno-defer-pop, -Wall, -I `ocamlc -where`, so CFLAGS could also be
simplified.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11358 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 16 insertions, 16 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 55b907adf7..5d3026605d 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -13,11 +13,11 @@
 
 #include <stdio.h>
 #include <stdlib.h> 
-#include <config.h>
-#include <misc.h>
-#include <mlvalues.h>
-#include <fail.h>
-#include <memory.h>
+#include <caml/config.h>
+#include <caml/misc.h>
+#include <caml/mlvalues.h>
+#include <caml/fail.h>
+#include <caml/memory.h>
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
 
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index 0034531836..c1a4e0ae66 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -12,7 +12,7 @@
 #ifndef _COQ_FIX_CODE_
 #define _COQ_FIX_CODE_
 
-#include <mlvalues.h>
+#include <caml/mlvalues.h>
 void * coq_stat_alloc (asize_t sz);
 
 #ifdef THREADED_CODE
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index ccccbe78d1..c7b18b9006 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -10,8 +10,8 @@
 
 #ifndef _COQ_CAML_GC_
 #define _COQ_CAML_GC_
-#include <mlvalues.h>
-#include <alloc.h>
+#include <caml/mlvalues.h>
+#include <caml/alloc.h>
 
 typedef void (*scanning_action) (value, value *);
 
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 880e978afb..98ef279112 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -21,7 +21,7 @@
 #include "coq_values.h" 
 
 /*spiwack : imports support functions for 64-bit integers */
-#include "config.h"
+#include <caml/config.h>
 #ifdef ARCH_INT64_TYPE
 #include "int64_native.h"
 #else
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index edd059488d..c0093a49ea 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -11,11 +11,11 @@
 #ifndef _COQ_MEMORY_
 #define _COQ_MEMORY_
 
-#include <config.h>
-#include <fail.h>
-#include <misc.h>
-#include <memory.h>
-#include <mlvalues.h>
+#include <caml/config.h>
+#include <caml/fail.h>
+#include <caml/misc.h>
+#include <caml/memory.h>
+#include <caml/mlvalues.h>
 
 
 #define Coq_stack_size (4096 * sizeof(value))
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 4c631fce37..1bf493e2c0 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -11,8 +11,8 @@
 #ifndef _COQ_VALUES_
 #define _COQ_VALUES_
 
-#include <alloc.h>
-#include <mlvalues.h>
+#include <caml/alloc.h>
+#include <caml/mlvalues.h>
 
 #define Default_tag 0
 #define Accu_tag 0