tactics/refine.mli


1
2
3
4
5
6
7
8


(*i $Id$ i*)

open Term
open Tacmach

val refine : (int * constr) list * constr -> tactic
val refine_tac : (int * constr) list * constr -> tactic