Uniformize exact hint resolution with others in eauto.

[ppedrot]

This is the equivalent of #21193 for eauto rather than TC eauto. En passant this shows that the code does not respect the transparent state provided by the hint database, since we inconditionally use the default flag argument.

[ppedrot]

@coqbot bench

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                      rocq-equations │    8.54     8.67  -1.50 │    60166305817     60137364474   0.05 │  398764   398288   0.12 │
│                           rocq-core │    6.74     6.82  -1.17 │    41635866765     41626709872   0.02 │  460836   457648   0.70 │
│                    coq-math-classes │   82.97    83.72  -0.90 │   503206750042    503246212150  -0.01 │  513952   514812  -0.17 │
│                         coq-coqutil │   46.27    46.63  -0.77 │   290139716228    290182267998  -0.01 │  565312   562660   0.47 │
│                       coq-fourcolor │ 1362.32  1372.83  -0.77 │ 12558514902273  12558538275336  -0.00 │ 1402224  1404148  -0.14 │
│                        coq-compcert │  299.17   300.93  -0.58 │  1967689055909   1967639934947   0.00 │ 1276244  1274796   0.11 │
│          rocq-metarocq-translations │   15.45    15.53  -0.52 │   109553999598    109555736893  -0.00 │  774176   774176   0.00 │
│                 rocq-mathcomp-field │  186.81   187.58  -0.41 │  1428244608641   1428235659934   0.00 │ 2791848  2791948  -0.00 │
│                  rocq-mathcomp-boot │   38.95    39.11  -0.41 │   230892449873    230913795028  -0.01 │  748472   746632   0.25 │
│                        coq-coqprime │   52.75    52.96  -0.40 │   359976847379    359997753608  -0.01 │  822804   822836  -0.00 │
│                 rocq-metarocq-utils │   23.82    23.91  -0.38 │   154193680869    154248657580  -0.04 │  599984   602592  -0.43 │
│           rocq-metarocq-safechecker │  311.46   312.58  -0.36 │  2328418590239   2328419608417  -0.00 │ 1866400  1874712  -0.44 │
│                   coq-iris-examples │  364.93   366.00  -0.29 │  2411466272754   2411511955283  -0.00 │ 1134648  1136188  -0.14 │
│ coq-neural-net-interp-computed-lite │  236.51   237.10  -0.25 │  2266855541782   2266842195429   0.00 │  846392   848436  -0.24 │
│                 rocq-metarocq-pcuic │  623.62   625.00  -0.22 │  3994368173508   3994022867592   0.01 │ 1885140  1917908  -1.71 │
│                         coq-unimath │ 1792.72  1796.68  -0.22 │ 14854483884487  14854332324552   0.00 │ 1083768  1079200   0.42 │
│              rocq-mathcomp-fingroup │   26.38    26.43  -0.19 │   172645627421    172611655800   0.02 │  602908   602904   0.00 │
│          coq-performance-tests-lite │  900.44   902.12  -0.19 │  7263178301374   7265515368141  -0.03 │ 2206164  2206512  -0.02 │
│                        coq-rewriter │  331.37   331.92  -0.17 │  2480738039845   2480714431098   0.00 │ 1439736  1437976   0.12 │
│                 coq-category-theory │  580.17   580.86  -0.12 │  4292307720766   4292592144223  -0.01 │  934156   936408  -0.24 │
│             rocq-mathcomp-character │  100.92   101.03  -0.11 │   720293473336    720440432569  -0.02 │ 2131284  2131184   0.00 │
│         coq-rewriter-perf-SuperFast │  476.47   476.91  -0.09 │  3728607149275   3727817857795   0.02 │ 1251756  1253996  -0.18 │
│        coq-fiat-crypto-with-bedrock │ 7221.38  7227.82  -0.09 │ 59686139782502  59690019175260  -0.01 │ 3255028  3253544   0.05 │
│                           coq-color │  229.40   229.58  -0.08 │  1454841820752   1454880288787  -0.00 │ 1160104  1160476  -0.03 │
│                            coq-corn │  647.59   647.78  -0.03 │  4383385051648   4383506262801  -0.00 │  743404   743932  -0.07 │
│              rocq-mathcomp-solvable │  102.64   102.66  -0.02 │   718265964268    718270531421  -0.00 │ 1527692  1527708  -0.00 │
│               coq-engine-bench-lite │  127.02   127.02   0.00 │   948325946874    948760969691  -0.05 │ 1084848  1084508   0.03 │
│             rocq-mathcomp-ssreflect │    1.18     1.18   0.00 │     8313609392      8315959207  -0.03 │  862668   865180  -0.29 │
│                rocq-metarocq-common │   40.42    40.42   0.00 │   260155435978    260159493846  -0.00 │  892684   893032  -0.04 │
│               coq-mathcomp-analysis │ 1046.12  1045.86   0.02 │  7906285248146   7907017845381  -0.01 │ 2585040  2585052  -0.00 │
│                             coq-vst │  835.39   835.14   0.03 │  6324179125386   6324412029856  -0.00 │ 2161884  2160080   0.08 │
│               rocq-mathcomp-algebra │  326.75   326.62   0.04 │  2434732147554   2435008353463  -0.01 │ 2050440  2051624  -0.06 │
│                        rocq-runtime │   74.46    74.43   0.04 │   539901993693    539856821054   0.01 │  514684   514936  -0.05 │
│               rocq-metarocq-erasure │  474.39   474.05   0.07 │  3244974196315   3244781830452   0.01 │ 1932516  1929144   0.17 │
│                      coq-verdi-raft │  496.92   496.53   0.08 │  3433642646558   3433785811593  -0.00 │  829616   829112   0.06 │
│                        coq-bedrock2 │  351.81   351.41   0.11 │  2918096187004   2918358626826  -0.01 │  840280   837372   0.35 │
│                       coq-fiat-core │   54.82    54.75   0.13 │   336013784012    336036651662  -0.01 │  484156   482096   0.43 │
│                      coq-coquelicot │   46.29    46.23   0.13 │   272220438268    272240547593  -0.01 │  837868   840000  -0.25 │
│              coq-mathcomp-odd-order │  601.19   600.16   0.17 │  4356596763561   4356792431506  -0.00 │ 3390384  3390300   0.00 │
│                    coq-fiat-parsers │  276.10   275.55   0.20 │  2114974569398   2114894400216   0.00 │ 2093448  2095696  -0.11 │
│              rocq-metarocq-template │   82.26    82.03   0.28 │   564750802256    564743797109   0.00 │ 1042924  1042424   0.05 │
│                         rocq-stdlib │  449.60   448.12   0.33 │  1544211326061   1544139214563   0.00 │  628508   626204   0.37 │
│                 rocq-mathcomp-order │   81.78    81.48   0.37 │   602219367851    602279423097  -0.01 │ 2063244  2060268   0.14 │
│                            coq-hott │  161.83   161.09   0.46 │  1106409237350   1106492612148  -0.01 │  493336   492980   0.07 │
│                            coq-core │    2.93     2.91   0.69 │    19732974758     19751629498  -0.09 │  106880   107032  -0.14 │
│                        rocq-bignums │   24.99    24.81   0.73 │   157713024538    157686188437   0.02 │  460388   460572  -0.04 │
│                           coq-verdi │   43.04    42.70   0.80 │   286041691408    286096190519  -0.02 │  527240   527532  -0.06 │
│                           rocq-elpi │   16.11    15.73   2.42 │   112212612117    112202247107   0.01 │  572924   573028  -0.02 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SLOW DOWNS                                                             │
│                                                                                                                                          │
│   OLD      NEW     DIFF     %DIFF     Ln                    FILE                                                                         │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│     62.2    64.8  2.5915      4.16%   608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │
│    7.567    8.52  0.9530     12.59%  1506  coq-vst/floyd/Component.v.html                                                                │
│   15.344  16.181  0.8370      5.45%  1223  coq-vst/floyd/Component.v.html                                                                │
│     2.42    3.20  0.7839     32.41%   607  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                     │
│     1.61    2.01  0.3965     24.61%    75  rocq-stdlib/theories/Numbers/HexadecimalString.v.html                                         │
│    0.124   0.510  0.3853    309.93%   270  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                            │
│     58.4    58.8  0.3842      0.66%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                      │
│     1.51    1.88  0.3697     24.42%   313  rocq-stdlib/theories/Strings/Byte.v.html                                                      │
│    0.607   0.967  0.3597     59.25%    41  rocq-stdlib/theories/ZArith/Zdiv_facts.v.html                                                 │
│     27.0    27.4  0.3349      1.24%   148  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                  │
│     20.9    21.2  0.3202      1.53%   479  rocq-metarocq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v.html              │
│     28.8    29.1  0.3094      1.07%   145  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                  │
│     19.9    20.2  0.2734      1.37%    40  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html  │
│     9.74    10.0  0.2676      2.75%   304  coq-fiat-crypto-with-bedrock/src/Fancy/Montgomery256.v.html                                   │
│     7.65    7.89  0.2367      3.09%    31  coq-performance-tests-lite/src/pattern.v.html                                                 │
│    0.365   0.595  0.2302     63.06%    11  rocq-stdlib/theories/omega/PreOmega.v.html                                                    │
│     21.2    21.4  0.2301      1.09%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                       │
│     18.7    18.9  0.2275      1.22%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                             │
│    0.315   0.532  0.2166     68.74%    11  rocq-stdlib/theories/Sorting/PermutEq.v.html                                                  │
│  0.00204   0.213  0.2112  10361.78%   262  rocq-metarocq-erasure/erasure/theories/Typed/Erasure.v.html                                   │
│     48.4    48.6  0.2084      0.43%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                   │
│    0.131   0.340  0.2083    158.50%    15  rocq-stdlib/theories/FSets/FMapInterface.v.html                                               │
│    0.381   0.586  0.2052     53.88%    18  rocq-stdlib/theories/FSets/FMapFacts.v.html                                                   │
│     28.8    29.0  0.1944      0.67%   530  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                    │
│ 0.000480   0.190  0.1900  39585.42%   124  rocq-metarocq-erasure/erasure/theories/EOptimizePropDiscr.v.html                              │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                TOP 25 SPEED UPS                                                                │
│                                                                                                                                                │
│  OLD    NEW     DIFF     %DIFF    Ln                      FILE                                                                                 │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  26.0    23.6  -2.3863   -9.19%   129  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html                                   │
│  95.5    93.8  -1.7169   -1.80%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│  94.9    93.8  -1.0932   -1.15%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│   237     236  -1.0620   -0.45%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│  94.8    93.8  -0.9504   -1.00%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  22.1    21.3  -0.7806   -3.54%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                               │
│  18.9    18.1  -0.7540   -3.99%    32  coq-performance-tests-lite/src/pattern.v.html                                                           │
│   178     177  -0.6843   -0.39%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│   134     133  -0.6410   -0.48%   155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│  31.5    31.0  -0.5456   -1.73%    12  coq-fourcolor/theories/proof/job254to270.v.html                                                         │
│  1.58    1.18  -0.4017  -25.42%  1142  rocq-stdlib/theories/FSets/FMapAVL.v.html                                                               │
│  47.0    46.6  -0.3966   -0.84%   115  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                              │
│  25.0    24.6  -0.3883   -1.55%    12  coq-fourcolor/theories/proof/job503to506.v.html                                                         │
│  29.5    29.2  -0.3754   -1.27%    12  coq-fourcolor/theories/proof/job589to610.v.html                                                         │
│  12.8    12.4  -0.3547   -2.78%   930  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html                   │
│ 0.449  0.0991  -0.3498  -77.93%   312  rocq-stdlib/theories/Reals/Abstract/ConstructiveAbs.v.html                                              │
│  31.3    30.9  -0.3366   -1.08%   180  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│ 0.515   0.180  -0.3349  -65.01%   592  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                               │
│  31.1    30.8  -0.3342   -1.07%   198  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│  25.5    25.2  -0.3267   -1.28%    12  coq-fourcolor/theories/proof/job535to541.v.html                                                         │
│  31.2    30.9  -0.3250   -1.04%   166  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│  33.2    32.9  -0.3246   -0.98%    12  coq-fourcolor/theories/proof/job439to465.v.html                                                         │
│  26.0    25.7  -0.3181   -1.22%    12  coq-fourcolor/theories/proof/job466to485.v.html                                                         │
│  30.2    29.8  -0.3154   -1.05%    12  coq-fourcolor/theories/proof/job001to106.v.html                                                         │
│  31.3    31.0  -0.3078   -0.98%   214  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job