Module Ltac_plugin.G_obligations

val set_default_tactic : ?loc:Loc.t -> Tactic_option.tac_option_locality -> Tacexpr.glob_tactic_expr -> unit
val get_default_tactic : unit -> unit Proofview.tactic
val print_default_tactic : unit -> Pp.t
val with_tac : ( Genarg.glob_generic_argument option -> 'a ) -> Tacexpr.raw_tactic_expr option -> 'b
module Tactic = Pltac
type 'a withtac_argtype = ( Tacexpr.raw_tactic_expr option, 'a ) Genarg.abstract_argument_type
val obligation : pm:Declare.OblState.t -> (int * Names.Id.t option * Constrexpr.constr_expr option) -> Tacexpr.raw_tactic_expr option -> Declare.Proof.t
val next_obligation : pm:Declare.OblState.t -> Names.Id.t option -> Tacexpr.raw_tactic_expr option -> Declare.Proof.t
val classify_obbl : 'a -> Vernacextend.vernac_classification