diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-13 23:07:54 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-13 23:07:54 +0000 |
| commit | 0e608025f45c9ffc2573c72e5c23bc183e3ab0b3 (patch) | |
| tree | 69d66976f12d7bc9f46e1ba681fa9401a8515226 /tactics/autorewrite.mli | |
| parent | e2655d38d11b072da0e5f4d40b05adbea73c8b8d (diff) | |
Rewrite of setoid_rewrite to modularize it based on proof-producing
strategies (à la ELAN).
Now setoid_rewrite is just one strategy and autorewrite is a
more elaborate one. Any kind of traversals can be defined, strategies
can be composed etc... in ML. An incomplete (no fix) language extension
for specifying them in Ltac is there too.
On a typical autorewrite-with-setoids usage, proof production time is
divided by 2 and proof size by 10.
Fix some admitted proofs and buggy patterns in Classes.Morphisms as
well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12081 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/autorewrite.mli')
| -rw-r--r-- | tactics/autorewrite.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index f0557f9d3..632a28170 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -9,6 +9,8 @@ (*i $Id$ i*) (*i*) +open Term +open Tacexpr open Tacmach (*i*) @@ -22,6 +24,11 @@ val add_rew_rules : string -> raw_rew_rule list -> unit val autorewrite : tactic -> string list -> tactic val autorewrite_in : Names.identifier -> tactic -> string list -> tactic +(* Rewriting rules *) +(* the type is the statement of the lemma constr. Used to elim duplicates. *) +type rew_rule = constr * types * bool * glob_tactic_expr + +val find_base : string -> rew_rule list val auto_multi_rewrite : string list -> Tacticals.clause -> tactic |