aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/backtrack.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/backtrack.ml')
-rw-r--r--toplevel/backtrack.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml
index 912d694eb..2d919e966 100644
--- a/toplevel/backtrack.ml
+++ b/toplevel/backtrack.ml
@@ -62,7 +62,7 @@ let npop n =
(* Since our history stack always contains an initial entry,
it's invalid to try to completely empty it *)
if n < 0 || n >= Stack.length history then raise Invalid
- else for i = 1 to n do pop () done
+ else for _i = 1 to n do pop () done
let top () =
try Stack.top history with Stack.Empty -> raise Invalid
@@ -107,7 +107,7 @@ let mark_command ast =
[pnum] and finally going to state number [snum]. *)
let raw_backtrack snum pnum naborts =
- for i = 1 to naborts do Pfedit.delete_current_proof () done;
+ for _i = 1 to naborts do Pfedit.delete_current_proof () done;
Pfedit.undo_todepth pnum;
Lib.reset_label snum