summaryrefslogtreecommitdiff
path: root/contrib/interface/blast.mli
blob: f670194399d17143d205a4a537e1751f2de53066 (plain)
1
2
3
val blast_tac : (Tacexpr.raw_tactic_expr -> 'a) ->
    int list -> Proof_type.tactic