From c86d78c0f18fb28f74bb6b192c03ebe73117cf03 Mon Sep 17 00:00:00 2001 From: bgregoir Date: Mon, 11 Dec 2006 18:46:35 +0000 Subject: 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 --- kernel/byterun/coq_fix_code.c | 10 +++++----- kernel/byterun/coq_fix_code.h | 2 +- kernel/byterun/coq_gc.h | 4 ++-- kernel/byterun/coq_interp.c | 6 +----- kernel/byterun/coq_interp.h | 4 ++++ kernel/byterun/coq_memory.c | 7 +------ kernel/byterun/coq_memory.h | 10 +++++----- kernel/byterun/coq_values.c | 2 +- kernel/byterun/coq_values.h | 4 ++-- 9 files changed, 22 insertions(+), 27 deletions(-) (limited to 'kernel/byterun') 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 #include -#include "config.h" -#include "misc.h" -#include "mlvalues.h" -#include "fail.h" -#include "memory.h" +#include +#include +#include +#include +#include #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 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 +#include 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 +#include +#include +#include +#include #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 /* 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 +#include #define Default_tag 0 #define Accu_tag 0 -- cgit v1.2.3