blob: 9215eced30b2c70a2910c2ec3b66f0f8eb7fc2db (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(*i $Id$ i*)
open Tacmach
open Term
(* Rewriting rules *)
type rew_rule = constr * bool * tactic
(* To add rewriting rules to a base *)
val add_rew_rules : string -> rew_rule list -> unit
(* The AutoRewrite tactic *)
val autorewrite : tactic -> string list -> tactic
|
