diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 8 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 |
2 files changed, 7 insertions, 3 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 171b1f75a8..2e9d30dfc4 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1213,9 +1213,13 @@ module Strategies = let try_ str : strategy = choice str id + let check_interrupt str e l c t r ev = + Control.check_for_interrupt (); + str e l c t r ev + let fix (f : strategy -> strategy) : strategy = - let rec aux env = f (fun env -> aux env) env in aux - + let rec aux env = f (fun env -> check_interrupt aux env) env in aux + let any (s : strategy) : strategy = fix (fun any -> try_ (seq s any)) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index fcce6e5eba..966d355d42 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -413,7 +413,7 @@ module New = struct let rec tclREPEAT0 t = tclINDEPENDENT begin tclIFCATCH t - (fun () -> tclREPEAT0 t) + (fun () -> tclCHECKINTERRUPT () <*> tclREPEAT0 t) (fun e -> catch_failerror e <*> tclUNIT ()) end let tclREPEAT t = |