Changement dans le kernel :

   - essai de suppression des dependances debiles. (echec) 
   - Application des patch debian.

Pour ring et field :
   - introduciton de la function de sign et de puissance.
   - Correction de certains bug.
   - supression de ring_replace ....

Pour exact_no_check :
   - ajout de la tactic : vm_cast_no_check (t)
     qui remplace "exact_no_check (t<: type of Goal)"
      (cette version forcais l'evaluation du cast dans le 
       pretypage).




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

9 files changed, 22 insertions, 27 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 70648b44b..affcccb3a 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -10,11 +10,11 @@
 
 #include <stdio.h>
 #include <stdlib.h> 
-#include "config.h"
-#include "misc.h"
-#include "mlvalues.h"
-#include "fail.h"
-#include "memory.h"
+#include <config.h>
+#include <misc.h>
+#include <mlvalues.h>
+#include <fail.h>
+#include <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 035d5b9b1..d1dac80fb 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 <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 2f0853264..ccccbe78d 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 <mlvalues.h>
+#include <alloc.h>
 
 typedef void (*scanning_action) (value, value *);
 
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0f91a7e3f..8f9c10e68 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -44,11 +44,7 @@ sp is a local copy of the global variable extern_sp. */
 #  ifdef DEBUG
 #    define Next goto next_instr
 #  else
-#    ifdef __ia64__
-#      define Next goto *(void *)(coq_jumptbl_base + *((uint32 *) pc)++)
-#    else
-#      define Next goto *(void *)(coq_jumptbl_base + *pc++)
-#    endif
+#    define Next goto *(void *)(coq_jumptbl_base + *pc++)  
 #  endif
 #else 
 #  define Instruct(name) case name:
diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h
index 76e689440..60865c32e 100644
--- a/kernel/byterun/coq_interp.h
+++ b/kernel/byterun/coq_interp.h
@@ -19,5 +19,9 @@ value coq_push_vstack(value stk);
 
 value  coq_interprete_ml(value tcode, value a, value e, value ea);
 
+value coq_interprete
+    (code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args);
+
 value coq_eval_tcode (value tcode, value e);
 
+
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index bfcb6812c..913421087 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -14,6 +14,7 @@
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
 #include "coq_memory.h"
+#include "coq_interp.h"
 
 /* stack */
 
@@ -264,9 +265,3 @@ value coq_set_drawinstr(value unit)
   return Val_unit;
 }
 
-
-value coq_print_pointer(value p)
-{
-  printf("pointer = %X\n", p);
-  return Val_unit;
-}
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index 0d866dc76..edd059488 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 <config.h>
+#include <fail.h>
+#include <misc.h>
+#include <memory.h>
+#include <mlvalues.h>
 
 
 #define Coq_stack_size (4096 * sizeof(value))
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 34b885e8f..007f61b27 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -13,7 +13,7 @@
 #include "coq_instruct.h"
 #include "coq_memory.h"
 #include "coq_values.h"
-#include "memory.h"
+#include <memory.h>
 /* KIND OF VALUES */
 
 #define Setup_for_gc
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index a5176f3f5..4c631fce3 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 <alloc.h>
+#include <mlvalues.h>
 
 #define Default_tag 0
 #define Accu_tag 0