aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof.ml')
-rw-r--r--proofs/proof.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 9f2c90c375..5f07cc1acc 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -398,8 +398,6 @@ let run_tactic env tac pr =
(*** Commands ***)
-let in_proof p k = k (Proofview.return p.proofview)
-
(* Remove all the goals from the shelf and adds them at the end of the
focused goals. *)
let unshelve p =