diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-14 22:37:17 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-14 22:37:17 +0000 |
| commit | b596e8303c0d22c5df1aed3c7a56b6af863a1b9e (patch) | |
| tree | d9f45775b586e63bdb1c0f5d859a74c7eb6e6fe3 /plugins/setoid_ring/Field_tac.v | |
| parent | c5e30bcb154f2f02706de8589055f60f1924fa51 (diff) | |
Rewrite autorewrite to use a dnet indexed by the left-hand sides (or
rhs) of rewrite lemmas for efficient retrieval of matching lemmas.
Autorewrite's implementation is still unchanged but the dnet can be used
through the [hints] strategy of the new generalized rewrite. Now lemmas
are checked to actually be rewriting lemmas at declaration time hence
the change in DoubleSqrt where some unapplicable constants were declared
as lemmas.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12087 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/setoid_ring/Field_tac.v')
0 files changed, 0 insertions, 0 deletions