aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/pfedit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r--proofs/pfedit.ml6
1 files changed, 1 insertions, 5 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 3dbb2190b..cad700b84 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -30,7 +30,7 @@ let undo n =
let p = Proof_global.give_me_the_proof () in
let d = Proof.V82.depth p in
if n >= d then raise Proof.EmptyUndoStack;
- for i = 1 to n do
+ for _i = 1 to n do
Proof.undo p
done
@@ -47,10 +47,6 @@ let undo_todepth n =
undo ((current_proof_depth ()) - n )
with Proof_global.NoCurrentProof when n=0 -> ()
-let set_undo _ = ()
-let get_undo _ = None
-
-
let start_proof id str hyps c ?init_tac ?compute_guard hook =
let goals = [ (Global.env_of_context hyps , c) ] in
let init_tac = Option.map Proofview.V82.tactic init_tac in