From 799f27ae19d6d2d16ade15bbdab83bd9acb0035f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 29 Jun 2015 21:33:50 +0200
Subject: class_tactics: make interruptible

Tracing with gdb by Alec Faithfull
---
 tactics/class_tactics.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 09cf4b0498..80f47c680f 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -490,6 +490,7 @@ let hints_tac hints =
 let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
   let rec aux s (acc : autogoal list list) fk = function
     | (gl,info) :: gls ->
+        Control.check_for_interrupt ();
 	(match info.is_evar with
 	 | Some ev when Evd.is_defined s ev -> aux s acc fk gls
 	 | _ ->
-- 
cgit v1.2.3