Module Ltac_plugin.ExtratacticsSource

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