From bf578ad5e2f63b7a36aeaef5e0597101db1bd24a Mon Sep 17 00:00:00 2001
From: gregoire
Date: Fri, 2 Dec 2005 10:01:15 +0000
Subject: Changement des named_context Ajout de cast indiquant au kernel la
 strategie a suivre Resolution du bug sur les coinductifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/byterun/coq_interp.c | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 48d91e4dcf..8bfe78ebee 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -55,7 +55,7 @@ sp is a local copy of the global variable extern_sp. */
 #  define Next break
 #endif 
 
-/*#define _COQ_DEBUG_ */
+/* #define _COQ_DEBUG_ */
 
 #ifdef _COQ_DEBUG_ 
 #   define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s)
@@ -715,7 +715,7 @@ value coq_interprete
 	  forcable = Val_true;
 	  /* On pousse l'addresse de retour et l'argument */
 	  sp -= 3;
-	  sp[0] = (value) (pc);
+	  sp[0] = (value) (pc - 1);
 	  sp[1] = coq_env;
 	  sp[2] = Val_long(coq_extra_args);
 	  /* On evalue le cofix */
@@ -966,6 +966,7 @@ value coq_push_vstack(value stk) {
 value  coq_interprete_ml(value tcode, value a, value e, value ea) {
   print_instr("coq_interprete");
   return coq_interprete((code_t)tcode, a, e, Long_val(ea));
+   print_instr("end coq_interprete");
 }
 
 value coq_eval_tcode (value tcode, value e) {
-- 
cgit v1.2.3