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