aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/rules.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 996deb8c5..986f2bebc 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -27,7 +27,7 @@ type lseqtac= global_reference -> seqtac
type 'a with_backtracking = tactic -> 'a
let wrap n b continue seq gls=
- check_for_interrupt ();
+ Control.check_for_interrupt ();
let nc=pf_hyps gls in
let env=pf_env gls in
let rec aux i nc ctx=