diff options
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index d844e8bf5..61da0c605 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3376,6 +3376,11 @@ sig end end +module Proof_bullet : +sig + val get_default_goal_selector : unit -> Vernacexpr.goal_selector +end + module Proof_global : sig type proof_mode = Proof_global.proof_mode = { @@ -3410,7 +3415,6 @@ sig (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit val compact_the_proof : unit -> unit val register_proof_mode : proof_mode -> unit - val get_default_goal_selector : unit -> Vernacexpr.goal_selector exception NoCurrentProof val give_me_the_proof : unit -> Proof.proof |