aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/tactic_debug.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ltac/tactic_debug.ml')
-rw-r--r--ltac/tactic_debug.ml8
1 files changed, 5 insertions, 3 deletions
diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml
index 5cbddc7f6..698c913e8 100644
--- a/ltac/tactic_debug.ml
+++ b/ltac/tactic_debug.ml
@@ -108,6 +108,8 @@ let string_get s i =
try Proofview.NonLogical.return (String.get s i)
with e -> Proofview.NonLogical.raise e
+let run_invalid_arg () = Proofview.NonLogical.raise (Invalid_argument "run_com")
+
(* Gives the number of steps or next breakpoint of a run command *)
let run_com inst =
let open Proofview.NonLogical in
@@ -118,14 +120,14 @@ let run_com inst =
let s = String.sub inst i (String.length inst - i) in
if inst.[0] >= '0' && inst.[0] <= '9' then
int_of_string s >>= fun num ->
- (if num<0 then invalid_arg "run_com" else return ()) >>
+ (if num<0 then run_invalid_arg () else return ()) >>
(skip:=num) >> (skipped:=0)
else
breakpoint:=Some (possibly_unquote s)
else
- invalid_arg "run_com"
+ run_invalid_arg ()
else
- invalid_arg "run_com"
+ run_invalid_arg ()
(* Prints the run counter *)
let run ini =