diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-06-29 21:33:50 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-06-29 22:16:07 +0200 |
| commit | 799f27ae19d6d2d16ade15bbdab83bd9acb0035f (patch) | |
| tree | ab20b4009e8acc461c9ace5380761f24f71ae0db | |
| parent | 38da14404781843a6143fc4af9d503e05d8d7dd6 (diff) | |
class_tactics: make interruptible
Tracing with gdb by Alec Faithfull
| -rw-r--r-- | tactics/class_tactics.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 09cf4b049..80f47c680 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 | _ -> |