aboutsummaryrefslogtreecommitdiff
path: root/tactics/autorewrite.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/autorewrite.mli')
-rw-r--r--tactics/autorewrite.mli11
1 files changed, 11 insertions, 0 deletions
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
new file mode 100644
index 0000000000..bbbc2b047c
--- /dev/null
+++ b/tactics/autorewrite.mli
@@ -0,0 +1,11 @@
+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