Remove the Const constructor of exprf

We instead use the [Op] constructor for constants.  This allows [exprf]
to not depend on the interpretation function; this means we don't need
to map over it to change the interpretation function.  This saves us
about 300 lines of code and about 30s of build time, total.

After     | File Name                                                              | Before    || Change
-----------------------------------------------------------------------------------------------------------
18m11.34s | Total                                                                  | 18m46.86s || -0m35.52s
-----------------------------------------------------------------------------------------------------------
0m19.99s  | Specific/GF25519ReflectiveAddCoordinates                               | 0m31.78s  || -0m11.79s
1m53.69s  | Specific/GF25519Reflective/Reified/LadderStep                          | 2m01.32s  || -0m07.62s
1m27.74s  | Specific/GF25519Reflective/Reified/AddCoordinates                      | 1m34.03s  || -0m06.29s
0m01.45s  | Specific/GF25519Reflective                                             | 0m06.31s  || -0m04.85s
0m04.62s  | Reflection/InlineInterp                                                | 0m01.52s  || +0m03.10s
1m19.68s  | CompleteEdwardsCurve/ExtendedCoordinates                               | 1m21.19s  || -0m01.50s
0m02.90s  | Reflection/InlineWf                                                    | 0m01.80s  || +0m01.09s
   N/A    | Reflection/MapWithInterpInfo                                           | 0m01.70s  || -0m01.70s
1m32.32s  | Test/Curve25519SpecTestVectors                                         | 1m32.25s  || +0m00.06s
1m12.79s  | Experiments/Ed25519                                                    | 1m13.17s  || -0m00.38s
0m40.52s  | ModularArithmetic/Conversion                                           | 0m40.44s  || +0m00.08s
0m34.57s  | Spec/Ed25519                                                           | 0m34.53s  || +0m00.03s
0m30.82s  | ModularArithmetic/ModularBaseSystemProofs                              | 0m30.89s  || -0m00.07s
0m30.11s  | Specific/GF25519Bounded                                                | 0m30.21s  || -0m00.10s
0m23.20s  | Experiments/MontgomeryCurve                                            | 0m23.26s  || -0m00.06s
0m22.16s  | Reflection/Z/Interpretations128/Relations                              | 0m21.72s  || +0m00.44s
0m21.69s  | ModularArithmetic/Pow2BaseProofs                                       | 0m21.58s  || +0m00.11s
0m20.25s  | Algebra                                                                | 0m20.27s  || -0m00.01s
0m19.81s  | Specific/GF25519                                                       | 0m19.83s  || -0m00.01s
0m18.82s  | Reflection/Z/Interpretations64/Relations                               | 0m18.50s  || +0m00.32s
0m18.19s  | EdDSARepChange                                                         | 0m18.26s  || -0m00.07s
0m17.08s  | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems                      | 0m17.16s  || -0m00.08s
0m14.10s  | Util/ZUtil                                                             | 0m14.03s  || +0m00.07s
0m10.05s  | Testbit                                                                | 0m10.02s  || +0m00.03s
0m08.95s  | Specific/GF25519BoundedCommon                                          | 0m08.90s  || +0m00.04s
0m08.87s  | BoundedArithmetic/ArchitectureToZLikeProofs                            | 0m08.81s  || +0m00.05s
0m08.80s  | Assembly/GF25519                                                       | 0m08.82s  || -0m00.01s
0m08.80s  | ModularArithmetic/Montgomery/ZProofs                                   | 0m08.87s  || -0m00.06s
0m08.51s  | Encoding/PointEncoding                                                 | 0m08.53s  || -0m00.01s
0m08.37s  | BoundedArithmetic/Double/Proofs/Multiply                               | 0m08.39s  || -0m00.02s
0m08.34s  | Specific/GF1305                                                        | 0m08.31s  || +0m00.02s
0m07.85s  | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate          | 0m07.86s  || -0m00.01s
0m07.60s  | Specific/GF25519Reflective/Reified/Mul                                 | 0m07.52s  || +0m00.08s
0m07.13s  | MxDHRepChange                                                          | 0m07.08s  || +0m00.04s
0m06.85s  | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate                    | 0m06.77s  || +0m00.08s
0m06.62s  | Reflection/Z/InterpretationsGen                                        | 0m06.62s  || +0m00.00s
0m05.69s  | Reflection/Z/Interpretations64/RelationsCombinations                   | 0m05.60s  || +0m00.09s
0m05.68s  | Reflection/Z/Interpretations128/RelationsCombinations                  | 0m05.67s  || +0m00.00s
0m05.48s  | Specific/SC25519                                                       | 0m05.38s  || +0m00.10s
0m05.40s  | BoundedArithmetic/Double/Proofs/RippleCarryAddSub                      | 0m05.36s  || +0m00.04s
0m04.93s  | ModularArithmetic/ModularBaseSystemListProofs                          | 0m04.96s  || -0m00.03s
0m04.87s  | WeierstrassCurve/Pre                                                   | 0m04.83s  || +0m00.04s
0m04.45s  | Specific/GF25519Reflective/Reified/PreFreeze                           | 0m04.56s  || -0m00.10s
0m04.33s  | Specific/GF25519Reflective/CommonBinOp                                 | 0m04.55s  || -0m00.21s
0m03.95s  | ModularArithmetic/BarrettReduction/ZHandbook                           | 0m03.98s  || -0m00.02s
0m03.87s  | Specific/GF25519Reflective/CommonUnOp                                  | 0m04.08s  || -0m00.20s
0m03.86s  | Encoding/PointEncodingPre                                              | 0m03.88s  || -0m00.02s
0m03.84s  | BaseSystemProofs                                                       | 0m03.88s  || -0m00.04s
0m03.75s  | Specific/GF25519Reflective/CommonUnOpWireToFE                          | 0m03.96s  || -0m00.20s
0m03.64s  | CompleteEdwardsCurve/Pre                                               | 0m03.60s  || +0m00.04s
0m03.51s  | BoundedArithmetic/InterfaceProofs                                      | 0m03.42s  || +0m00.08s
0m03.41s  | ModularArithmetic/Tutorial                                             | 0m03.38s  || +0m00.03s
0m03.30s  | Reflection/LinearizeWf                                                 | 0m04.24s  || -0m00.94s
0m03.20s  | Specific/GF25519Reflective/Reified/CarrySub                            | 0m03.28s  || -0m00.07s
0m03.14s  | ModularArithmetic/ZBoundedZ                                            | 0m03.14s  || +0m00.00s
0m03.14s  | ModularArithmetic/BarrettReduction/ZGeneralized                        | 0m03.14s  || +0m00.00s
0m02.95s  | Specific/GF25519Reflective/Reified/CarryAdd                            | 0m02.93s  || +0m00.02s
0m02.92s  | Specific/GF25519Reflective/Common9_4Op                                 | 0m02.89s  || +0m00.02s
0m02.82s  | Specific/GF25519Reflective/Reified/CarryOpp                            | 0m02.95s  || -0m00.13s
0m02.82s  | BoundedArithmetic/Double/Proofs/Decode                                 | 0m02.90s  || -0m00.08s
0m02.69s  | BoundedArithmetic/Double/Proofs/ShiftRight                             | 0m02.69s  || +0m00.00s
0m02.66s  | ModularArithmetic/ModularArithmeticTheorems                            | 0m02.67s  || -0m00.00s
0m02.63s  | Specific/FancyMachine256/Montgomery                                    | 0m02.24s  || +0m00.38s
0m02.61s  | Specific/GF25519Reflective/CommonUnOpFEToWire                          | 0m02.76s  || -0m00.14s
0m02.58s  | BoundedArithmetic/Double/Proofs/ShiftLeft                              | 0m02.58s  || +0m00.00s
0m02.56s  | Specific/GF25519Reflective/Common                                      | 0m02.60s  || -0m00.04s
0m02.52s  | Specific/FancyMachine256/Barrett                                       | 0m02.20s  || +0m00.31s
0m02.50s  | Specific/GF25519BoundedAddCoordinates                                  | 0m02.60s  || -0m00.10s
0m02.39s  | ModularArithmetic/BarrettReduction/ZBounded                            | 0m02.31s  || +0m00.08s
0m02.34s  | ModularArithmetic/ModularBaseSystemOpt                                 | 0m02.31s  || +0m00.02s
0m02.02s  | Specific/GF25519Reflective/Reified/Sub                                 | 0m02.01s  || +0m00.01s
0m01.98s  | Reflection/WfReflective                                                | 0m02.54s  || -0m00.56s
0m01.94s  | Specific/GF25519Reflective/Reified/Pack                                | 0m02.07s  || -0m00.12s
0m01.93s  | Assembly/Evaluables                                                    | 0m01.93s  || +0m00.00s
0m01.92s  | Specific/GF25519Reflective/Reified/Unpack                              | 0m02.04s  || -0m00.12s
0m01.90s  | Specific/FancyMachine256/Core                                          | 0m01.79s  || +0m00.10s
0m01.79s  | ModularArithmetic/Montgomery/ZBounded                                  | 0m01.86s  || -0m00.07s
0m01.77s  | Specific/GF25519ExtendedAddCoordinates                                 | 0m01.76s  || +0m00.01s
0m01.68s  | Specific/GF25519Reflective/Reified/Add                                 | 0m01.69s  || -0m00.01s
0m01.67s  | Specific/GF25519BoundedExtendedAddCoordinates                          | 0m01.79s  || -0m00.12s
0m01.63s  | Experiments/Ed25519Extraction                                          | 0m01.66s  || -0m00.03s
0m01.62s  | Specific/GF25519Reflective/Reified/Opp                                 | 0m01.72s  || -0m00.09s
0m01.54s  | Specific/GF25519Reflective/Reified/GeModulus                           | 0m01.59s  || -0m00.05s
0m01.50s  | Reflection/TestCase                                                    | 0m01.42s  || +0m00.08s
0m01.47s  | ModularArithmetic/BarrettReduction/Z                                   | 0m01.47s  || +0m00.00s
0m01.43s  | Assembly/Compile                                                       | 0m01.46s  || -0m00.03s
0m01.33s  | Reflection/WfProofs                                                    | 0m01.95s  || -0m00.61s
0m01.26s  | ModularArithmetic/PrimeFieldTheorems                                   | 0m01.28s  || -0m00.02s
0m01.20s  | Assembly/Conversions                                                   | 0m01.19s  || +0m00.01s
0m01.16s  | ModularArithmetic/ExtendedBaseVector                                   | 0m01.22s  || -0m00.06s
0m01.16s  | BaseSystem                                                             | 0m01.15s  || +0m00.01s
0m01.09s  | BoundedArithmetic/Double/Repeated/Proofs/Decode                        | 0m01.11s  || -0m00.02s
0m00.99s  | Util/NumTheoryUtil                                                     | 0m00.96s  || +0m00.03s
0m00.96s  | Assembly/HL                                                            | 0m00.96s  || +0m00.00s
0m00.94s  | Assembly/LL                                                            | 0m00.99s  || -0m00.05s
0m00.94s  | Assembly/Pipeline                                                      | 0m00.92s  || +0m00.01s
0m00.88s  | Reflection/WfInversion                                                 | 0m01.21s  || -0m00.32s
0m00.86s  | Assembly/PhoasCommon                                                   | 0m00.91s  || -0m00.05s
0m00.86s  | Specific/GF25519Reflective/CommonUnOpFEToZ                             | 0m01.02s  || -0m00.16s
0m00.85s  | BoundedArithmetic/Double/Proofs/LoadImmediate                          | 0m00.86s  || -0m00.01s
0m00.84s  | BoundedArithmetic/Double/Proofs/BitwiseOr                              | 0m00.91s  || -0m00.07s
0m00.82s  | BoundedArithmetic/X86ToZLikeProofs                                     | 0m00.85s  || -0m00.03s
0m00.79s  | Util/IterAssocOp                                                       | 0m00.82s  || -0m00.02s
0m00.75s  | Reflection/Z/Syntax                                                    | 0m00.67s  || +0m00.07s
0m00.73s  | Util/PartiallyReifiedProp                                              | 0m00.73s  || +0m00.00s
0m00.70s  | Encoding/ModularWordEncodingTheorems                                   | 0m00.76s  || -0m00.06s
0m00.70s  | Specific/GF25519Reflective/Reified                                     | 0m00.72s  || -0m00.02s
0m00.66s  | BoundedArithmetic/Double/Repeated/Proofs/Multiply                      | 0m00.62s  || +0m00.04s
0m00.66s  | ModularArithmetic/PseudoMersenneBaseParamProofs                        | 0m00.66s  || +0m00.00s
0m00.64s  | Encoding/ModularWordEncodingPre                                        | 0m00.63s  || +0m00.01s
0m00.61s  | ModularArithmetic/ModularBaseSystem                                    | 0m00.66s  || -0m00.05s
0m00.61s  | Util/AdditionChainExponentiation                                       | 0m00.64s  || -0m00.03s
0m00.60s  | ModularArithmetic/ExtPow2BaseMulProofs                                 | 0m00.64s  || -0m00.04s
0m00.60s  | Reflection/MultiSizeTest2                                              | 0m00.71s  || -0m00.10s
0m00.60s  | Spec/EdDSA                                                             | 0m00.65s  || -0m00.05s
0m00.59s  | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub             | 0m00.51s  || +0m00.07s
0m00.58s  | BoundedArithmetic/Interface                                            | 0m00.60s  || -0m00.02s
0m00.58s  | ModularArithmetic/ModularBaseSystemList                                | 0m00.61s  || -0m00.03s
0m00.55s  | Spec/ModularWordEncoding                                               | 0m00.63s  || -0m00.07s
0m00.55s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight                | 0m00.50s  || +0m00.05s
0m00.55s  | Reflection/InterpWfRel                                                 | 0m00.58s  || -0m00.02s
0m00.54s  | BoundedArithmetic/X86ToZLike                                           | 0m00.55s  || -0m00.01s
0m00.54s  | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional             | 0m00.53s  || +0m00.01s
0m00.54s  | BoundedArithmetic/Double/Proofs/SelectConditional                      | 0m00.62s  || -0m00.07s
0m00.54s  | Reflection/WfReflectiveGen                                             | 0m00.58s  || -0m00.03s
0m00.52s  | BoundedArithmetic/ArchitectureToZLike                                  | 0m00.41s  || +0m00.11s
0m00.51s  | BoundedArithmetic/Double/Core                                          | 0m00.48s  || +0m00.03s
0m00.50s  | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr                     | 0m00.51s  || -0m00.01s
0m00.49s  | Spec/WeierstrassCurve                                                  | 0m00.42s  || +0m00.07s
0m00.48s  | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate                 | 0m00.54s  || -0m00.06s
0m00.47s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.58s  || -0m00.10s
0m00.47s  | Reflection/InterpWf                                                    | 0m00.50s  || -0m00.03s
0m00.47s  | ModularArithmetic/Pre                                                  | 0m00.48s  || -0m00.01s
0m00.47s  | BoundedArithmetic/Double/Repeated/Core                                 | 0m00.46s  || +0m00.00s
0m00.46s  | Reflection/Z/Interpretations64                                         | 0m00.49s  || -0m00.02s
0m00.45s  | Reflection/InputSyntax                                                 | 0m00.42s  || +0m00.03s
   N/A    | Reflection/MapInterpWf                                                 | 0m00.44s  || -0m00.44s
0m00.44s  | Spec/CompleteEdwardsCurve                                              | 0m00.39s  || +0m00.04s
0m00.44s  | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic                   | 0m00.42s  || +0m00.02s
0m00.44s  | Reflection/Z/Interpretations128                                        | 0m00.52s  || -0m00.08s
0m00.44s  | ModularArithmetic/ZBounded                                             | 0m00.45s  || -0m00.01s
0m00.42s  | BoundedArithmetic/StripCF                                              | 0m00.42s  || +0m00.00s
0m00.42s  | Reflection/Z/Reify                                                     | 0m00.43s  || -0m00.01s
0m00.42s  | ModularArithmetic/ModularBaseSystemListZOperationsProofs               | 0m00.47s  || -0m00.04s
0m00.41s  | Reflection/Named/DeadCodeElimination                                   | 0m00.43s  || -0m00.02s
0m00.41s  | ModularArithmetic/PseudoMersenneBaseParams                             | 0m00.38s  || +0m00.02s
0m00.41s  | Spec/ModularArithmetic                                                 | 0m00.34s  || +0m00.06s
0m00.41s  | Reflection/Named/RegisterAssign                                        | 0m00.37s  || +0m00.03s
0m00.41s  | Reflection/Reify                                                       | 0m00.39s  || +0m00.01s
0m00.40s  | ModularArithmetic/Pow2Base                                             | 0m00.42s  || -0m00.01s
0m00.40s  | Reflection/Named/EstablishLiveness                                     | 0m00.33s  || +0m00.07s
0m00.40s  | Reflection/ExprInversion                                               | 0m00.57s  || -0m00.16s
0m00.40s  | Reflection/Named/Syntax                                                | 0m00.40s  || +0m00.00s
0m00.38s  | Reflection/Named/Compile                                               | 0m00.34s  || +0m00.03s
   N/A    | Reflection/MapInterp                                                   | 0m00.38s  || -0m00.38s
0m00.38s  | ModularArithmetic/Montgomery/Z                                         | 0m00.39s  || -0m00.01s
0m00.38s  | ModularArithmetic/ModularBaseSystemWord                                | 0m00.36s  || +0m00.02s
   N/A    | Reflection/WfRel                                                       | 0m00.38s  || -0m00.38s
0m00.38s  | Reflection/Tuple                                                       |    N/A    || +0m00.38s
0m00.37s  | Spec/MxDH                                                              | 0m00.39s  || -0m00.02s
0m00.37s  | BoundedArithmetic/Eta                                                  | 0m00.36s  || +0m00.01s
0m00.36s  | Reflection/Named/ContextOn                                             | 0m00.37s  || -0m00.01s
0m00.34s  | Reflection/FilterLive                                                  | 0m00.34s  || +0m00.00s
0m00.34s  | Reflection/LinearizeInterp                                             | 0m00.53s  || -0m00.19s
0m00.33s  | Reflection/Relations                                                   |    N/A    || +0m00.33s
0m00.32s  | Reflection/Equality                                                    | 0m00.41s  || -0m00.08s
0m00.30s  | Reflection/Syntax                                                      | 0m00.52s  || -0m00.22s
0m00.30s  | Reflection/InterpProofs                                                | 0m00.47s  || -0m00.17s
0m00.30s  | Reflection/ApplicationLemmas                                           | 0m00.43s  || -0m00.13s
0m00.30s  | Reflection/CommonSubexpressionElimination                              | 0m00.50s  || -0m00.20s
0m00.28s  | Reflection/Inline                                                      | 0m00.37s  || -0m00.08s
0m00.28s  | Reflection/Conversion                                                  | 0m00.44s  || -0m00.15s
0m00.27s  | Reflection/MapCastWithCastOp                                           | 0m00.38s  || -0m00.10s
0m00.26s  | Reflection/MapCast                                                     | 0m00.40s  || -0m00.14s
0m00.26s  | Reflection/ApplicationRelations                                        | 0m00.35s  || -0m00.08s
0m00.24s  | Reflection/Application                                                 | 0m00.38s  || -0m00.14s
0m00.23s  | Reflection/Linearize                                                   | 0m00.35s  || -0m00.11s
0m00.20s  | Reflection/CountLets                                                   | 0m00.33s  || -0m00.13s
0m00.20s  | Reflection/Named/NameUtil                                              | 0m00.36s  || -0m00.15s
0m00.09s  | Util/PointedProp                                                       | 0m00.08s  || +0m00.00s
0m00.05s  | Util/LetIn                                                             | 0m00.06s  || -0m00.00s
0m00.03s  | Util/Notations                                                         | 0m00.03s  || +0m00.00s
0m00.03s  | Util/AutoRewrite                                                       | 0m00.03s  || +0m00.00s

1 files changed, 1 insertions, 0 deletions

diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index 4eadbdf26..3f8c6810c 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -9,6 +9,7 @@ Require Export Crypto.Util.GlobalSettings.
     Coq's parser. *)
 
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Reserved Notation "()" (at level 0).
 Reserved Infix "=?" (at level 70, no associativity).
 Reserved Infix "!=?" (at level 70, no associativity).
 Reserved Infix "?=" (at level 70, no associativity).