package coq
Module Funind_plugin.InvfunSource
Source
val invfun :
Tactypes.quantified_hypothesis ->
Names.GlobRef.t option ->
unit Proofview.tactic