G_obligations
val wit_withtac : Gentactic.raw_generic_tactic option Genarg.vernac_genarg_type
val withtac : Gentactic.raw_generic_tactic option Procq.Entry.t