diff options
author | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-11 18:46:35 +0000 |
---|---|---|
committer | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-11 18:46:35 +0000 |
commit | c86d78c0f18fb28f74bb6b192c03ebe73117cf03 (patch) | |
tree | 99294164215016607e4056e5730a2d6c91043dbf /kernel/byterun/coq_memory.c | |
parent | 70c88a5f6d7e1ef184d70512969a6221eec8d11e (diff) |
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
Diffstat (limited to 'kernel/byterun/coq_memory.c')
-rw-r--r-- | kernel/byterun/coq_memory.c | 7 |
1 files changed, 1 insertions, 6 deletions
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; -} |