Remove WBW Mont lemmas from push_eval

autorewrite is slow and not customiziable enough.

1 files changed, 0 insertions, 11 deletions

diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v
index 7e9701f47..f3c6fa709 100644
--- a/src/Experiments/NewPipeline/Arithmetic.v
+++ b/src/Experiments/NewPipeline/Arithmetic.v
@@ -4282,15 +4282,4 @@ Module WordByWordMontgomery.
             = eval a mod m).
     Proof. apply to_bytesmod_correct. Qed.
   End modops.
-  Hint Rewrite
-       eval_onemod
-       eval_from_montgomerymod
-       eval_mulmod
-       eval_squaremod
-       eval_encodemod
-       eval_addmod
-       eval_submod
-       eval_oppmod
-       eval_to_bytesmod
-    : push_eval.
 End WordByWordMontgomery.