Add databases for ring_simplify

After    | File Name                                         | Before   || Change
------------------------------------------------------------------------------------
2m39.49s | Total                                             | 2m36.24s || +0m03.25s
------------------------------------------------------------------------------------
0m48.49s | Specific/GF25519                                  | 0m48.53s || -0m00.03s
0m34.52s | CompleteEdwardsCurve/ExtendedCoordinates          | 0m34.24s || +0m00.28s
0m15.71s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m15.24s || +0m00.47s
0m11.41s | Experiments/SpecEd25519                           | 0m11.34s || +0m00.07s
0m08.23s | Specific/GF1305                                   | 0m08.30s || -0m00.07s
0m05.64s | Algebra                                           | 0m05.55s || +0m00.08s
0m05.03s | WeierstrassCurve/Pre                              | 0m04.51s || +0m00.52s
0m04.23s | ModularArithmetic/Tutorial                        | 0m03.63s || +0m00.60s
0m03.33s | CompleteEdwardsCurve/Pre                          | 0m03.34s || -0m00.00s
0m02.87s | ModularArithmetic/ModularBaseSystemOpt            | 0m02.80s || +0m00.07s
0m01.80s | Experiments/EdDSARefinement                       | 0m01.77s || +0m00.03s
0m01.54s | ModularArithmetic/PrimeFieldTheorems              | 0m01.55s || -0m00.01s
0m01.52s | Encoding/PointEncodingPre                         | 0m01.54s || -0m00.02s
0m01.51s | ModularArithmetic/ModularArithmeticTheorems       | 0m01.51s || +0m00.00s
0m01.19s | ModularArithmetic/ExtendedBaseVector              | 0m01.18s || +0m00.01s
0m01.16s | ModularArithmetic/ModularBaseSystemListProofs     | 0m00.80s || +0m00.35s
0m01.03s | ModularArithmetic/ModularBaseSystemProofs         | 0m00.96s || +0m00.07s
0m00.95s | Experiments/SpecificCurve25519                    | 0m00.95s || +0m00.00s
0m00.92s | Experiments/DerivationsOptionRectLetInEncoding    | 0m00.85s || +0m00.07s
0m00.91s | ModularArithmetic/ModularBaseSystemField          | 0m00.86s || +0m00.05s
0m00.76s | Encoding/ModularWordEncodingPre                   | 0m00.60s || +0m00.16s
0m00.69s | Util/IterAssocOp                                  | 0m00.67s || +0m00.01s
0m00.69s | ModularArithmetic/ModularBaseSystemList           | 0m00.57s || +0m00.12s
0m00.68s | ModularArithmetic/ExtPow2BaseMulProofs            | 0m00.63s || +0m00.05s
0m00.68s | Spec/EdDSA                                        | 0m00.61s || +0m00.07s
0m00.67s | Encoding/ModularWordEncodingTheorems              | 0m00.64s || +0m00.03s
0m00.66s | Spec/ModularWordEncoding                          | 0m00.56s || +0m00.09s
0m00.62s | Util/AdditionChainExponentiation                  | 0m00.59s || +0m00.03s
0m00.58s | ModularArithmetic/ModularBaseSystem               | 0m00.57s || +0m00.01s
0m00.55s | ModularArithmetic/PseudoMersenneBaseParamProofs   | 0m00.54s || +0m00.01s
0m00.51s | Spec/WeierstrassCurve                             | 0m00.43s || +0m00.08s
0m00.41s | Spec/CompleteEdwardsCurve                         | 0m00.38s || +0m00.02s

1 files changed, 8 insertions, 0 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index 153871d4c..f4afcb935 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -1307,6 +1307,14 @@ Ltac ring_simplify_subterms := tac_on_subterms ltac:(fun t => ring_simplify t).
 Ltac ring_simplify_subterms_in_all :=
   reverse_nondep; ring_simplify_subterms; intros.
 
+Create HintDb ring_simplify discriminated.
+Create HintDb ring_simplify_subterms discriminated.
+Create HintDb ring_simplify_subterms_in_all discriminated.
+Hint Extern 1 => progress ring_simplify : ring_simplify.
+Hint Extern 1 => progress ring_simplify_subterms : ring_simplify_subterms.
+Hint Extern 1 => progress ring_simplify_subterms_in_all : ring_simplify_subterms_in_all.
+
+
 Section Example.
   Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
   Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div.