tactics/refine.mli


1
2
3
4
5
6
7
8


(* $Id$ *)

open Term
open Tacmach

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