diff options
Diffstat (limited to 'tactics/autorewrite.mli')
| -rw-r--r-- | tactics/autorewrite.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 8b18f23f2c..cc4c5ed37b 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -20,5 +20,6 @@ val add_rew_rules : string -> raw_rew_rule list -> unit (* The AutoRewrite tactic *) val autorewrite : tactic -> string list -> tactic +val autorewrite_in : Names.identifier -> tactic -> string list -> tactic val print_rewrite_hintdb : string -> unit |