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