diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e9fbece4d..b7018fe45 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -989,7 +989,7 @@ let rec val_interp ist (tac:glob_tactic_expr) : typed_generic_argument GTac.t = (** Delayed evaluation *) GTac.return (of_tacvalue (VFun (extract_trace ist, ist.lfun, [], t))) in - check_for_interrupt (); + Control.check_for_interrupt (); match curr_debug ist with | DebugOn lev -> let eval v = |