Make the library 20% faster: [auto with *] is evil

I do hereby revoke the privilege of [intuition] to grab random hints
from random databases.  This privilege is reserved for
[debug_intuition], which comes with a warning about not being used in
production code.  This tactic is useful in conjunction with `Print Hint
*`, to discover what hint databases the hints were grabbed from.

(Suggestions for renaming [debug_intuition] welcome.)

Any file using [intuition] must [Require Export
Crypto.Util.FixCoqMistakes.].  It's possible we could lift this
restriction by compiling [FixCoqMistakes] separately, and passing along
`-require FixCoqMistakes` to Coq.  Should we do this?

After    | File Name                                         | Before   || Change
------------------------------------------------------------------------------------
3m29.54s | Total                                             | 4m33.13s || -1m03.59s
------------------------------------------------------------------------------------
0m03.75s | BaseSystemProofs                                  | 0m43.84s || -0m40.09s
0m42.57s | CompleteEdwardsCurve/ExtendedCoordinates          | 0m34.48s || +0m08.09s
0m03.04s | Util/ListUtil                                     | 0m11.18s || -0m08.14s
0m01.62s | ModularArithmetic/PrimeFieldTheorems              | 0m09.53s || -0m07.90s
0m00.87s | Util/NumTheoryUtil                                | 0m07.61s || -0m06.74s
0m01.61s | Encoding/PointEncodingPre                         | 0m06.93s || -0m05.31s
0m51.95s | Specific/GF25519                                  | 0m47.52s || +0m04.42s
0m12.30s | Experiments/SpecEd25519                           | 0m11.29s || +0m01.01s
0m09.22s | Specific/GF1305                                   | 0m08.17s || +0m01.05s
0m03.48s | CompleteEdwardsCurve/Pre                          | 0m04.77s || -0m01.28s
0m02.70s | Assembly/State                                    | 0m04.09s || -0m01.38s
0m01.55s | ModularArithmetic/ModularArithmeticTheorems       | 0m02.93s || -0m01.38s
0m01.16s | Assembly/Pseudize                                 | 0m02.34s || -0m01.17s
0m15.67s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m16.37s || -0m00.70s
0m06.02s | Algebra                                           | 0m06.67s || -0m00.65s
0m05.90s | Experiments/GenericFieldPow                       | 0m06.68s || -0m00.77s
0m04.65s | WeierstrassCurve/Pre                              | 0m05.27s || -0m00.61s
0m03.93s | ModularArithmetic/Pow2BaseProofs                  | 0m03.94s || -0m00.00s
0m03.70s | ModularArithmetic/Tutorial                        | 0m03.85s || -0m00.14s
0m02.83s | ModularArithmetic/ModularBaseSystemOpt            | 0m02.84s || -0m00.00s
0m02.74s | Experiments/EdDSARefinement                       | 0m01.80s || +0m00.94s
0m02.35s | Util/ZUtil                                        | 0m02.51s || -0m00.15s
0m01.86s | Assembly/Wordize                                  | 0m02.32s || -0m00.45s
0m01.23s | ModularArithmetic/ExtendedBaseVector              | 0m01.20s || +0m00.03s
0m01.21s | BaseSystem                                        | 0m01.63s || -0m00.41s
0m01.03s | Experiments/SpecificCurve25519                    | 0m00.98s || +0m00.05s
0m01.01s | ModularArithmetic/ModularBaseSystemProofs         | 0m01.11s || -0m00.10s
0m00.95s | ModularArithmetic/BarrettReduction/Z              | 0m01.38s || -0m00.42s
0m00.92s | Experiments/DerivationsOptionRectLetInEncoding    | 0m01.81s || -0m00.89s
0m00.85s | ModularArithmetic/ModularBaseSystemField          | 0m00.86s || -0m00.01s
0m00.82s | ModularArithmetic/ModularBaseSystemListProofs     | 0m00.79s || +0m00.02s
0m00.80s | Assembly/QhasmEvalCommon                          | 0m00.93s || -0m00.13s
0m00.73s | Spec/EdDSA                                        | 0m00.59s || +0m00.14s
0m00.72s | Util/Tuple                                        | 0m00.71s || +0m00.01s
0m00.70s | Util/IterAssocOp                                  | 0m00.72s || -0m00.02s
0m00.67s | Encoding/ModularWordEncodingTheorems              | 0m00.71s || -0m00.03s
0m00.66s | Assembly/Pipeline                                 | 0m00.64s || +0m00.02s
0m00.65s | Testbit                                           | 0m00.65s || +0m00.00s
0m00.65s | Assembly/PseudoConversion                         | 0m00.65s || +0m00.00s
0m00.64s | Util/AdditionChainExponentiation                  | 0m00.63s || +0m00.01s
0m00.63s | ModularArithmetic/ExtPow2BaseMulProofs            | 0m00.64s || -0m00.01s
0m00.63s | Assembly/Pseudo                                   | 0m00.65s || -0m00.02s
0m00.62s | ModularArithmetic/ModularBaseSystem               | 0m00.57s || +0m00.05s
0m00.61s | ModularArithmetic/ModularBaseSystemList           | 0m00.57s || +0m00.04s
0m00.60s | Encoding/ModularWordEncodingPre                   | 0m00.69s || -0m00.08s
0m00.60s | ModularArithmetic/PseudoMersenneBaseParamProofs   | 0m00.59s || +0m00.01s
0m00.56s | Assembly/StringConversion                         | 0m00.56s || +0m00.00s
0m00.54s | Spec/ModularWordEncoding                          | 0m00.61s || -0m00.06s
0m00.54s | Assembly/QhasmUtil                                | 0m00.46s || +0m00.08s
0m00.52s | Assembly/Qhasm                                    | 0m00.53s || -0m00.01s
0m00.48s | Assembly/AlmostQhasm                              | 0m00.52s || -0m00.04s
0m00.48s | ModularArithmetic/Pre                             | 0m00.48s || +0m00.00s
0m00.46s | Assembly/Vectorize                                | 0m00.72s || -0m00.25s
0m00.45s | Spec/WeierstrassCurve                             | 0m00.44s || +0m00.01s
0m00.44s | Assembly/AlmostConversion                         | 0m00.44s || +0m00.00s
0m00.43s | ModularArithmetic/Pow2Base                        | 0m00.51s || -0m00.08s
0m00.42s | ModularArithmetic/PseudoMersenneBaseParams        | 0m00.38s || +0m00.03s
0m00.41s | Spec/CompleteEdwardsCurve                         | 0m00.43s || -0m00.02s
0m00.34s | Spec/ModularArithmetic                            | 0m00.36s || -0m00.01s
0m00.03s | Util/FixCoqMistakes                               |   N/A    || +0m00.03s
0m00.02s | Util/Notations                                    | 0m00.04s || -0m00.02s
0m00.02s | Util/Tactics                                      | 0m00.02s || +0m00.00s

1 files changed, 1 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 187ea6541..f4a6f121b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -64,6 +64,7 @@ src/Tactics/Algebra_syntax/Nsatz.v
 src/Util/AdditionChainExponentiation.v
 src/Util/CaseUtil.v
 src/Util/Decidable.v
+src/Util/FixCoqMistakes.v
 src/Util/IterAssocOp.v
 src/Util/ListUtil.v
 src/Util/NatUtil.v