Imported Upstream version 8.3.pl2upstream/8.3.pl2

3 files changed, 21 insertions, 4 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 98ef2791..cce2319b 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -14,6 +14,7 @@
    for fast computation of bounded (31bits) integers */
 
 #include <stdio.h>
+#include <signal.h>
 #include "coq_gc.h"
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
@@ -157,6 +158,12 @@ sp is a local copy of the global variable extern_sp. */
 #endif
 #endif
 
+/* For signal handling, we highjack some code from the caml runtime */
+
+extern intnat caml_signals_are_pending;
+extern intnat caml_pending_signals[];
+extern void caml_process_pending_signals(void);
+
 /* The interpreter itself */
 
 value coq_interprete
@@ -414,8 +421,13 @@ value coq_interprete
 	realloc_coq_stack(Coq_stack_threshold);
 	sp = coq_sp;
       }
+      /* We also check for signals */
+      if (caml_signals_are_pending) {
+	/* If there's a Ctrl-C, we reset the vm */
+	if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; }
+	caml_process_pending_signals();
+      }
       Next;
-      /* Fall through CHECK_SIGNALS */
 
       Instruct(APPTERM) {
 	int nargs = *pc++;
diff --git a/kernel/names.ml b/kernel/names.ml
index 9f1becf7..e5a9f0fc 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: names.ml 13486 2010-10-03 17:01:43Z herbelin $ *)
+(* $Id: names.ml 13804 2011-01-27 00:41:34Z letouzey $ *)
 
 open Pp
 open Util
@@ -223,7 +223,7 @@ type constructor = inductive * int
 
 let constant_of_kn kn = (kn,kn)
 let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
-let make_con mp dir l = ((mp,dir,l),(mp,dir,l))
+let make_con mp dir l = constant_of_kn (mp,dir,l)
 let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
 let canonical_con con = snd con
 let user_con con = fst con
@@ -235,6 +235,10 @@ let debug_pr_con con = str "("++ pr_kn (fst con) ++ str ","++ pr_kn (snd con)++
 let eq_constant (_,kn1) (_,kn2) = kn1=kn2
 let debug_string_of_con con =  string_of_kn (fst con)^"'"^string_of_kn (snd con)
 
+let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl =
+  if lbl = l1 && lbl = l2 then con
+  else ((mp1,dp1,lbl),(mp2,dp2,lbl))
+
 let con_modpath con = modpath (fst con)
 
 let mind_modpath mind = modpath (fst mind)
diff --git a/kernel/names.mli b/kernel/names.mli
index f54df6ec..f57116f9 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: names.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: names.mli 13804 2011-01-27 00:41:34Z letouzey $ i*)
 
 (*s Identifiers *)
 
@@ -139,6 +139,7 @@ val user_con : constant -> kernel_name
 val canonical_con : constant -> kernel_name
 val repr_con : constant -> module_path * dir_path * label
 val eq_constant : constant -> constant -> bool
+val con_with_label : constant -> label -> constant
 
 val string_of_con : constant -> string
 val con_label : constant -> label