diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-04 16:13:28 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-04 16:13:28 +0000 |
| commit | 038f4e1c7f572198cbf9c3b66384a308538ea6bc (patch) | |
| tree | 6c19534507328079543b7f2070248d2143deb647 /tactics/autorewrite.mli | |
| parent | fe008055f8adc7acd6af1483a8e7fef98d27e267 (diff) | |
Start documenting new [rewrite_strat] tactic that applies rewriting
according to a given strategy.
- Enhance the hints/lemmas strategy to support "using tac" comming from
rewrite hints to solve side-conditions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16558 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/autorewrite.mli')
| -rw-r--r-- | tactics/autorewrite.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 773e3694e..9ddabc584 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -12,7 +12,7 @@ open Tacmach open Equality (** Rewriting rules before tactic interpretation *) -type raw_rew_rule = Loc.t * Term.constr * bool * Tacexpr.raw_tactic_expr +type raw_rew_rule = Loc.t * Term.constr * bool * Tacexpr.raw_tactic_expr option (** To add rewriting rules to a base *) val add_rew_rules : string -> raw_rew_rule list -> unit @@ -29,7 +29,7 @@ type rew_rule = { rew_lemma: constr; rew_type: types; rew_pat: constr; rew_l2r: bool; - rew_tac: glob_tactic_expr } + rew_tac: glob_tactic_expr option } val find_rewrites : string -> rew_rule list |