diff options
| -rw-r--r-- | src/Experiments/NewPipeline/Arithmetic.v | 11 |
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. |