Module Ltac_plugin.G_obligations

val set_default_tactic : Vernacexpr.locality_flag -> Tacexpr.glob_tactic_expr -> unit
val get_default_tactic : unit -> Vernacexpr.locality_flag * unit Proofview.tactic
val print_default_tactic : unit -> Pp.t
val with_tac : (Genarg.glob_generic_argument option -> 'a) -> Tacexpr.raw_tactic_expr option -> 'a
module Tactic = Pltac
val sigref : Loc.t -> Constrexpr.constr_expr
type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
val wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type
val withtac : Tacexpr.raw_tactic_expr option Pcoq.Entry.t
val obligation : pstate:Proof_global.t option -> (int * Names.Id.t option * Constrexpr.constr_expr option) -> Tacexpr.raw_tactic_expr option -> Proof_global.t option
val next_obligation : pstate:Proof_global.t option -> Names.Id.t option -> Tacexpr.raw_tactic_expr option -> Proof_global.t option
val classify_obbl : 'a -> Vernacextend.vernac_type * Vernacextend.vernac_when