Funind_plugin.Invfun
val invfun : Tactypes.quantified_hypothesis -> Names.GlobRef.t option -> unit Proofview.tactic