aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_bullet.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof_bullet.mli')
-rw-r--r--proofs/proof_bullet.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index 9ae521d3f..9e924fec9 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -48,6 +48,6 @@ val suggest : proof -> Pp.t
(* *)
(**********************************************************)
-val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds
+val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t
val get_default_goal_selector : unit -> Vernacexpr.goal_selector