(* $Id$ *)

open Term
open Tacmach

val refine : constr -> tactic
val refine_tac : constr -> tactic