Module `Ltac_plugin.Extratactics`

val discrHyp : Names.Id.t -> unit Proofview.tactic
val injHyp : Names.Id.t -> unit Proofview.tactic
val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tactypes.delayed_open option -> unit Proofview.tactic