diff options
Diffstat (limited to 'tactics/autorewrite.mli')
| -rw-r--r-- | tactics/autorewrite.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 6196b04e..07065717 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -6,12 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This files implements the autorewrite tactic. *) + open Term open Tacexpr open Equality (** Rewriting rules before tactic interpretation *) -type raw_rew_rule = Loc.t * Term.constr Univ.in_universe_context_set * bool * Tacexpr.raw_tactic_expr option +type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option (** To add rewriting rules to a base *) val add_rew_rules : string -> raw_rew_rule list -> unit @@ -29,7 +31,7 @@ type rew_rule = { rew_lemma: constr; rew_pat: constr; rew_ctx: Univ.universe_context_set; rew_l2r: bool; - rew_tac: glob_tactic_expr option } + rew_tac: Genarg.glob_generic_argument option } val find_rewrites : string -> rew_rule list |