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