aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--CHANGES6
-rw-r--r--kernel/byterun/coq_interp.c2
2 files changed, 7 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index 80bf99538..0054e4cef 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,6 +12,12 @@ Changes from V8.3 to V8.4
implicit arguments aren't taken into account in partial applications. Use eta
expansion.
+- Coqide now runs coqtop as separated process, making it more robust:
+ coqtop subprocess can be interrupted (TODO check Win32), or even
+ killed and relaunched (cf button "Restart Coq", ex-"Go to Start").
+
+- Vm_compute can now be interrupted via Ctrl-C.
+
Tactics
- New tactics constr_eq, is_evar and has_evar.
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 842ac5619..df5806891 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -151,7 +151,7 @@ sp is a local copy of the global variable extern_sp. */
#endif
#endif
-/* For signal handling, we highjack some code from the caml runtime */
+/* For signal handling, we hijack some code from the caml runtime */
extern intnat caml_signals_are_pending;
extern intnat caml_pending_signals[];