aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun/coq_interp.h
diff options
context:
space:
mode:
authorGravatar bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-12-11 18:46:35 +0000
committerGravatar bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-12-11 18:46:35 +0000
commitc86d78c0f18fb28f74bb6b192c03ebe73117cf03 (patch)
tree99294164215016607e4056e5730a2d6c91043dbf /kernel/byterun/coq_interp.h
parent70c88a5f6d7e1ef184d70512969a6221eec8d11e (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_interp.h')
-rw-r--r--kernel/byterun/coq_interp.h4
1 files changed, 4 insertions, 0 deletions
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);
+