G_obligations (coq-core.Ltac_plugin.G

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

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 : 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