summaryrefslogtreecommitdiff
path: root/contrib/interface/debug_tac.mli
blob: da4bbaa0938a68382a5be9e56370dd46529758d3 (plain)
1
2
3
4
5
6

val report_error : Tacexpr.glob_tactic_expr ->
    Proof_type.goal Evd.sigma option ref ->
    Tacexpr.glob_tactic_expr ref -> int list ref -> int list -> Tacmach.tactic;;

val clean_path : Tacexpr.glob_tactic_expr -> int list -> int list;;