pbp.mli « interface « contrib - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/contrib/interface/pbp.mli

blob: 9daba1844cefbd671d6eb8ac4a438084295beeed (plain)

1 2	`val pbp_tac : (Tacexpr.raw_tactic_expr -> 'a) -> Names.identifier option -> int list -> Proof_type.tactic`