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

1 files changed, 2 insertions, 4 deletions

diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index 00c7aeec6..c72abed61 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -269,10 +269,8 @@ Section DoubleSqrt.
  Let spec_ww_Bm1 : [[wwBm1]] = wwB - 1.
  Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed.
 
- 
- Hint Rewrite spec_w_0 spec_w_1 w_Bm1 spec_w_WW spec_w_sub 
-              spec_w_div21 spec_w_add_mul_div spec_ww_Bm1
-              spec_w_add_c spec_w_sqrt2: w_rewrite.
+ Hint Rewrite spec_w_0 spec_w_1 spec_w_WW spec_w_sub
+   spec_w_add_mul_div spec_ww_Bm1 spec_w_add_c : w_rewrite.
 
  Lemma spec_ww_is_even : forall x,
       if ww_is_even x then [[x]] mod 2 = 0 else [[x]] mod 2 = 1.