clean elliptic curve proofs, use par: in WeierstrassAffineProofs

This required working fsatz around
<https://coq.inria.fr/bugs/show_bug.cgi?id=5452>;
par: abstract (abstract tac) raises anomalies

Curves/Weierstrass/AffineProofs is still affected by something like
<https://coq.inria.fr/bugs/show_bug.cgi?id=4831>;
par: Goals randomly not solved

The timing script ran out of memory the first time, so I winged the last
couple of files that were left.

src/Curves/Weierstrass/AffineProofs (real: 516.30, user: 757.86, sys: 2.52, mem: 2808940 ko), was: 14m49s
src/Curves/Montgomery/AffineProofs (real: 51.38, user: 50.82, sys: 0.48, mem: 1509924 ko),    was:    55s
src/Curves/Edwards/Montgomery (real: 4.55, user: 4.43, sys: 0.09, mem: 542008 ko),            was:     5s
src/Curves/Montgomery/XZProofs (real: 36.27, user: 35.87, sys: 0.32, mem: 1391216 ko),        was:    39s
src/Specific/IntegrationTestLadderstep (real: 158.95, user: 158.42, sys: 0.50, mem: 1827860 ko)was: 3m10s

0m43.48s  | Specific/IntegrationTestLadderstep                           | 3m10.35s  || -2m00.87s
3m08.45s  | Curves/Weierstrass/Projective                                | 2m39.76s  || +0m00.68s
2m13.43s  | Spec/Test/X25519                                             | 2m11.48s  || +0m00.95s
1m23.64s  | Specific/IntegrationTestLadderstep130                        | 1m20.78s  || +0m00.85s
1m05.88s  | Compilers/Z/ArithmeticSimplifierWf                           | 1m01.03s  || +0m00.84s
1m01.96s  | Spec/Ed25519                                                 | 0m55.02s  || +0m00.93s
0m33.80s  | Curves/Edwards/XYZT                                          | 0m25.10s  || +0m00.69s
0m30.97s  | Curves/Edwards/AffineProofs                                  | 0m29.76s  || +0m00.20s
0m24.12s  | Compilers/Named/MapCastWf                                    | 0m24.19s  || -0m00.07s
0m23.94s  | Primitives/EdDSARepChange                                    | 0m23.28s  || +0m00.66s
0m23.52s  | Util/ZUtil                                                   | 0m22.27s  || +0m00.25s
0m18.63s  | Compilers/Named/ContextProperties/SmartMap                   | 0m17.26s  || +0m00.36s
0m18.44s  | Compilers/Named/ContextProperties/NameUtil                   | 0m17.95s  || +0m00.49s
0m16.18s  | Specific/IntegrationTestMul                                  | 0m16.41s  || -0m00.23s
0m15.14s  | Compilers/Z/ArithmeticSimplifierInterp                       | 0m14.43s  || +0m00.71s
0m14.41s  | Algebra/Field                                                | 0m15.30s  || -0m00.89s
0m14.18s  | Specific/IntegrationTestSquare                               | 0m14.60s  || -0m00.41s
0m14.08s  | Compilers/CommonSubexpressionEliminationWf                   | 0m14.07s  || +0m00.00s
0m13.82s  | Specific/ArithmeticSynthesisTest                             | 0m10.24s  || +0m00.58s
0m13.34s  | Specific/IntegrationTestSub                                  | 0m13.49s  || -0m00.15s
0m11.72s  | Primitives/MxDHRepChange                                     | 0m11.02s  || +0m00.70s
0m11.30s  | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy          | 0m11.49s  || -0m00.18s
0m11.17s  | Arithmetic/MontgomeryReduction/Proofs                        | 0m10.42s  || +0m00.75s
0m11.13s  | Compilers/Named/MapCastInterp                                | 0m11.12s  || +0m00.01s
0m10.54s  | LegacyArithmetic/ArchitectureToZLikeProofs                   | 0m11.01s  || -0m00.47s
0m10.21s  | Compilers/InlineWf                                           | 0m11.00s  || -0m00.78s
0m10.21s  | LegacyArithmetic/Double/Proofs/Multiply                      | 0m10.51s  || -0m00.29s
0m10.07s  | Specific/ArithmeticSynthesisTest130                          | 0m06.78s  || +0m00.29s
0m09.96s  | Compilers/Named/RegisterAssignInterp                         | 0m10.03s  || -0m00.06s
0m09.70s  | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m10.77s  || -0m00.07s
0m08.93s  | Arithmetic/Core                                              | 0m08.42s  || +0m00.50s
0m08.87s  | Algebra/Ring                                                 | 0m08.99s  || -0m00.12s
0m08.61s  | Util/FixedWordSizesEquality                                  | 0m08.39s  || +0m00.21s
0m08.15s  | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate           | 0m08.99s  || -0m00.83s
0m07.97s  | Bedrock/Word                                                 | 0m07.77s  || +0m00.20s
0m07.92s  | Compilers/LinearizeWf                                        | 0m08.05s  || -0m00.13s
0m07.04s  | Util/ListUtil                                                | 0m06.56s  || +0m00.48s
0m06.78s  | Curves/Edwards/Pre                                           | 0m06.90s  || -0m00.12s
0m06.76s  | LegacyArithmetic/Pow2BaseProofs                              | 0m06.88s  || -0m00.12s
0m06.60s  | LegacyArithmetic/Double/Proofs/RippleCarryAddSub             | 0m06.60s  || +0m00.00s
0m05.80s  | Algebra/Field_test                                           | 0m06.11s  || -0m00.31s
0m04.49s  | Compilers/EtaWf                                              | 0m04.42s  || +0m00.07s
0m04.39s  | Util/ForLoop/Unrolling                                       | 0m04.52s  || -0m00.12s
0m04.32s  | Arithmetic/BarrettReduction/HAC                              | 0m04.39s  || -0m00.06s
0m04.26s  | Compilers/Named/CompileWf                                    | 0m04.50s  || -0m00.24s
0m04.25s  | LegacyArithmetic/InterfaceProofs                             | 0m03.92s  || +0m00.33s
0m04.13s  | Compilers/WfProofs                                           | 0m03.88s  || +0m00.25s
0m04.07s  | Compilers/TestCase                                           | 0m04.19s  || -0m00.12s
0m03.92s  | Arithmetic/Saturated                                         | 0m04.18s  || -0m00.25s
0m03.91s  | Specific/FancyMachine256/Montgomery                          | 0m03.86s  || +0m00.05s
0m03.69s  | LegacyArithmetic/ZBoundedZ                                   | 0m03.43s  || +0m00.25s
0m03.68s  | Curves/Montgomery/Affine                                     | 0m03.38s  || +0m00.30s
0m03.62s  | Arithmetic/ModularArithmeticTheorems                         | 0m03.35s  || +0m00.27s
0m03.51s  | Specific/FancyMachine256/Barrett                             | 0m03.47s  || +0m00.03s
0m03.43s  | Compilers/Named/CompileInterp                                | 0m03.47s  || -0m00.04s
0m03.37s  | Arithmetic/BarrettReduction/Generalized                      | 0m03.49s  || -0m00.12s
0m03.29s  | LegacyArithmetic/Double/Proofs/ShiftLeft                     | 0m04.16s  || -0m00.87s
0m03.27s  | Spec/MontgomeryCurve                                         | 0m03.57s  || -0m00.29s
0m03.26s  | Compilers/Named/ContextProperties                            | 0m03.18s  || +0m00.07s
0m03.12s  | Compilers/InlineInterp                                       | 0m03.16s  || -0m00.04s
0m03.09s  | LegacyArithmetic/Double/Proofs/ShiftRight                    | 0m04.30s  || -0m00.20s
0m02.97s  | LegacyArithmetic/Double/Proofs/Decode                        | 0m03.05s  || -0m00.07s
0m02.89s  | Compilers/Z/Bounds/Relax                                     | 0m02.76s  || +0m00.13s
0m02.86s  | Compilers/Named/NameUtilProperties                           | 0m02.86s  || +0m00.00s
0m02.79s  | Compilers/CommonSubexpressionEliminationProperties           | 0m02.68s  || +0m00.10s
0m02.77s  | Compilers/Z/Bounds/InterpretationLemmas/PullCast             | 0m02.73s  || +0m00.04s
0m02.63s  | LegacyArithmetic/BarretReduction                             | 0m02.50s  || +0m00.12s
0m02.59s  | Specific/FancyMachine256/Core                                | 0m02.21s  || +0m00.37s
0m02.32s  | Util/ForLoop/InvariantFramework                              | 0m02.15s  || +0m00.16s
0m02.28s  | Util/WordUtil                                                | 0m02.36s  || -0m00.08s
0m02.27s  | Compilers/WfReflective                                       | 0m02.19s  || +0m00.08s
0m02.04s  | Spec/WeierstrassCurve                                        | 0m00.61s  || +0m00.43s
0m01.95s  | LegacyArithmetic/MontgomeryReduction                         | 0m01.80s  || +0m00.14s
   N/A    | Curves/Weierstrass/Pre                                       | 0m01.94s  || -0m00.94s
0m01.82s  | Util/NatUtil                                                 | 0m01.80s  || +0m00.02s
0m01.71s  | Arithmetic/BarrettReduction/Wikipedia                        | 0m01.72s  || -0m00.01s
0m01.71s  | Compilers/Z/Bounds/Pipeline/Definition                       | 0m01.52s  || +0m00.18s
0m01.65s  | Util/Tuple                                                   | 0m01.64s  || +0m00.01s
0m01.64s  | Arithmetic/PrimeFieldTheorems                                | 0m01.67s  || -0m00.03s
0m01.59s  | Compilers/Named/InterpretToPHOASWf                           | 0m01.60s  || -0m00.01s
0m01.55s  | Algebra/Group                                                | 0m01.51s  || +0m00.04s
0m01.54s  | Compilers/Z/Syntax/Equality                                  | 0m01.48s  || +0m00.06s
0m01.26s  | Compilers/Relations                                          | 0m01.25s  || +0m00.01s
0m01.18s  | Compilers/LinearizeInterp                                    | 0m01.35s  || -0m00.17s
0m01.13s  | Compilers/WfInversion                                        | 0m01.02s  || +0m00.10s
0m01.09s  | Algebra/IntegralDomain                                       | 0m01.50s  || -0m00.40s
0m01.05s  | Compilers/Named/CompileProperties                            | 0m00.93s  || +0m00.12s
0m01.04s  | Util/NumTheoryUtil                                           | 0m01.01s  || +0m00.03s
0m01.02s  | Compilers/Named/InterpretToPHOASInterp                       | 0m00.90s  || +0m00.12s
0m00.98s  | LegacyArithmetic/Double/Proofs/BitwiseOr                     | 0m00.95s  || +0m00.03s
0m00.97s  | Util/PartiallyReifiedProp                                    | 0m00.93s  || +0m00.03s
0m00.97s  | LegacyArithmetic/Double/Proofs/LoadImmediate                 | 0m01.09s  || -0m00.12s
0m00.93s  | Specific/IntegrationTestTemporaryMiscCommon                  | 0m00.86s  || +0m00.07s
0m00.86s  | Compilers/Z/CNotations                                       | 0m00.82s  || +0m00.04s
0m00.85s  | Arithmetic/Karatsuba                                         | 0m00.87s  || -0m00.02s
0m00.85s  | Compilers/Z/Syntax/Util                                      | 0m00.75s  || +0m00.09s
0m00.84s  | LegacyArithmetic/BaseSystemProofs                            | 0m00.89s  || -0m00.05s
0m00.80s  | Compilers/MapCastByDeBruijnInterp                            | 0m00.99s  || -0m00.18s
0m00.78s  | Compilers/MultiSizeTest                                      | 0m00.78s  || +0m00.00s
0m00.75s  | Util/IterAssocOp                                             | 0m00.70s  || +0m00.05s
0m00.74s  | Util/ZUtil/Stabilization                                     | 0m00.74s  || +0m00.00s
0m00.73s  | LegacyArithmetic/Interface                                   | 0m00.64s  || +0m00.08s
0m00.67s  | Compilers/WfReflectiveGen                                    | 0m00.62s  || +0m00.05s
0m00.67s  | Util/CPSUtil                                                 | 0m00.58s  || +0m00.09s
0m00.67s  | Compilers/Z/Bounds/Pipeline/ReflectiveTactics                | 0m00.70s  || -0m00.02s
0m00.67s  | Curves/Montgomery/XZ                                         | 0m00.57s  || +0m00.10s
0m00.66s  | Compilers/MapCastByDeBruijnWf                                | 0m00.71s  || -0m00.04s
0m00.64s  | Compilers/InterpByIsoProofs                                  | 0m00.60s  || +0m00.04s
0m00.63s  | Compilers/Z/JavaNotations                                    | 0m00.62s  || +0m00.01s
0m00.62s  | Arithmetic/ModularArithmeticPre                              | 0m00.54s  || +0m00.07s
0m00.61s  | Spec/CompleteEdwardsCurve                                    | 0m00.60s  || +0m00.01s
0m00.60s  | Util/HList                                                   | 0m00.53s  || +0m00.06s
0m00.59s  | Util/Decidable                                               | 0m00.63s  || -0m00.04s
0m00.59s  | Compilers/CommonSubexpressionEliminationInterp               | 0m00.80s  || -0m00.21s
0m00.58s  | Compilers/Z/CommonSubexpressionElimination                   | 0m00.54s  || +0m00.03s
0m00.58s  | LegacyArithmetic/Double/Proofs/SelectConditional             | 0m00.90s  || -0m00.32s
0m00.57s  | Compilers/InterpWfRel                                        | 0m00.60s  || -0m00.03s
0m00.57s  | Compilers/Named/AListContext                                 | 0m00.53s  || +0m00.03s
0m00.57s  | Util/AdditionChainExponentiation                             | 0m00.51s  || +0m00.05s
0m00.56s  | Compilers/Z/Bounds/RoundUpLemmas                             | 0m00.59s  || -0m00.02s
0m00.56s  | Compilers/InputSyntax                                        | 0m00.54s  || +0m00.02s
0m00.55s  | Compilers/Named/FMapContext                                  | 0m00.55s  || +0m00.00s
0m00.55s  | Curves/Weierstrass/Affine                                    | 0m00.61s  || -0m00.05s
0m00.54s  | Spec/EdDSA                                                   | 0m00.53s  || +0m00.01s
0m00.54s  | Compilers/Z/Bounds/Pipeline                                  | 0m00.55s  || -0m00.01s
0m00.53s  | Compilers/Z/Bounds/InterpretationLemmas/Tactics              | 0m00.45s  || +0m00.08s
0m00.53s  | LegacyArithmetic/Double/Core                                 | 0m00.51s  || +0m00.02s
0m00.53s  | Compilers/CommonSubexpressionElimination                     | 0m00.51s  || +0m00.02s
0m00.51s  | Util/NUtil                                                   | 0m00.53s  || -0m00.02s
0m00.51s  | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic          | 0m00.47s  || +0m00.04s
0m00.51s  | Util/ForLoop/Tests                                           | 0m00.45s  || +0m00.06s
0m00.51s  | Compilers/Z/Reify                                            | 0m00.52s  || -0m00.01s
0m00.51s  | Compilers/Z/Bounds/MapCastByDeBruijnInterp                   | 0m00.50s  || +0m00.01s
0m00.50s  | LegacyArithmetic/ZBounded                                    | 0m00.51s  || -0m00.01s
0m00.50s  | Compilers/Z/ArithmeticSimplifier                             | 0m00.47s  || +0m00.03s
0m00.50s  | LegacyArithmetic/ArchitectureToZLike                         | 0m00.49s  || +0m00.01s
0m00.49s  | Compilers/InterpWf                                           | 0m00.49s  || +0m00.00s
0m00.49s  | Compilers/Z/Bounds/Interpretation                            | 0m00.47s  || +0m00.02s
0m00.48s  | Specific/IntegrationTestDisplayCommon                        | 0m00.45s  || +0m00.02s
0m00.47s  | Spec/ModularArithmetic                                       | 0m00.41s  || +0m00.06s
0m00.47s  | Compilers/Z/Bounds/MapCastByDeBruijn                         | 0m00.47s  || +0m00.00s
0m00.47s  | Compilers/Z/Bounds/Pipeline/Glue                             | 0m00.49s  || -0m00.02s
0m00.46s  | Algebra/Nsatz                                                | 0m00.62s  || -0m00.15s
0m00.46s  | Compilers/Reify                                              | 0m00.45s  || +0m00.01s
0m00.46s  | Compilers/Z/CommonSubexpressionEliminationWf                 | 0m00.48s  || -0m00.01s
0m00.46s  | Compilers/Z/MapCastByDeBruijnInterp                          | 0m00.47s  || -0m00.00s
0m00.46s  | Compilers/Z/Bounds/MapCastByDeBruijnWf                       | 0m00.49s  || -0m00.02s
0m00.45s  | LegacyArithmetic/BaseSystem                                  | 0m00.44s  || +0m00.01s
0m00.45s  | Util/ZRange                                                  | 0m00.44s  || +0m00.01s
0m00.45s  | Util/BoundedWord                                             | 0m00.43s  || +0m00.02s
0m00.44s  | Util/Factorize                                               | 0m00.57s  || -0m00.12s
0m00.44s  | Compilers/Z/Syntax                                           | 0m00.44s  || +0m00.00s
0m00.44s  | Compilers/Z/CommonSubexpressionEliminationInterp             | 0m00.59s  || -0m00.14s
0m00.44s  | Compilers/Z/MapCastByDeBruijnWf                              | 0m00.45s  || -0m00.01s
0m00.43s  | Compilers/Z/Inline                                           | 0m00.39s  || +0m00.03s
0m00.43s  | Compilers/Named/PositiveContext/DefaultsProperties           | 0m00.44s  || -0m00.01s
0m00.42s  | Compilers/Z/HexNotationConstants                             | 0m00.43s  || -0m00.01s
0m00.42s  | LegacyArithmetic/Pow2Base                                    | 0m00.42s  || +0m00.00s
0m00.42s  | Compilers/Z/FoldTypes                                        | 0m00.38s  || +0m00.03s
0m00.42s  | Compilers/Z/InlineInterp                                     | 0m00.40s  || +0m00.01s
0m00.42s  | Compilers/Z/MapCastByDeBruijn                                | 0m00.45s  || -0m00.03s
0m00.41s  | Compilers/Tuple                                              | 0m00.41s  || +0m00.00s
0m00.41s  | Compilers/Z/ArithmeticSimplifierUtil                         | 0m00.44s  || -0m00.03s
0m00.40s  | Compilers/Named/DeadCodeElimination                          | 0m00.39s  || +0m00.01s
0m00.39s  | Arithmetic/MontgomeryReduction/Definition                    | 0m00.43s  || -0m00.03s
0m00.39s  | Compilers/Z/Bounds/Pipeline/OutputType                       | 0m00.42s  || -0m00.02s
0m00.39s  | Compilers/Z/InlineWf                                         | 0m00.41s  || -0m00.01s
0m00.38s  | Compilers/Named/EstablishLiveness                            | 0m00.40s  || -0m00.02s
0m00.37s  | Compilers/Z/BinaryNotationConstants                          | 0m00.38s  || -0m00.01s
0m00.37s  | Compilers/Named/WeakListContext                              | 0m00.35s  || +0m00.02s
0m00.36s  | Compilers/FilterLive                                         | 0m00.36s  || +0m00.00s
0m00.36s  | Algebra/ScalarMult                                           | 0m00.33s  || +0m00.02s
0m00.35s  | Bedrock/Nomega                                               | 0m00.39s  || -0m00.04s
0m00.34s  | Util/FixedWordSizes                                          | 0m00.34s  || +0m00.00s
0m00.34s  | Compilers/Named/WfInterp                                     | 0m00.32s  || +0m00.02s
0m00.34s  | Compilers/Named/PositiveContext                              | 0m00.33s  || +0m00.01s
0m00.33s  | Compilers/ExprInversion                                      | 0m00.32s  || +0m00.01s
0m00.32s  | Util/ForLoop/Instances                                       | 0m00.34s  || -0m00.02s
0m00.32s  | Algebra/Monoid                                               | 0m00.29s  || +0m00.03s
0m00.31s  | Compilers/Equality                                           | 0m00.29s  || +0m00.02s
0m00.31s  | Compilers/Z/OpInversion                                      | 0m00.38s  || -0m00.07s
0m00.31s  | Compilers/Named/RegisterAssign                               | 0m00.32s  || -0m00.01s
0m00.31s  | Compilers/MapCastByDeBruijn                                  | 0m00.31s  || +0m00.00s
0m00.30s  | Algebra/Hierarchy                                            | 0m00.32s  || -0m00.02s
0m00.30s  | Compilers/Named/PositiveContext/Defaults                     | 0m00.29s  || +0m00.01s
0m00.29s  | Util/Sum                                                     | 0m00.30s  || -0m00.01s
0m00.29s  | Spec/MxDH                                                    | 0m00.26s  || +0m00.02s
0m00.28s  | Compilers/SmartMap                                           | 0m00.28s  || +0m00.00s
0m00.27s  | Compilers/EtaInterp                                          | 0m00.26s  || +0m00.01s
0m00.26s  | Compilers/Named/ContextDefinitions                           | 0m00.22s  || +0m00.04s
0m00.24s  | Compilers/CommonSubexpressionEliminationDenote               | 0m00.24s  || +0m00.00s
0m00.23s  | Util/ForLoop                                                 | 0m00.22s  || +0m00.01s
0m00.23s  | Compilers/Named/ContextOn                                    | 0m00.25s  || -0m00.01s
0m00.21s  | Util/LetInMonad                                              | 0m00.20s  || +0m00.00s
0m00.21s  | Compilers/Named/ContextProperties/Tactics                    | 0m00.23s  || -0m00.02s
0m00.20s  | Compilers/InterpProofs                                       | 0m00.22s  || -0m00.01s
0m00.17s  | Util/Sigma                                                   | 0m00.10s  || +0m00.07s
0m00.17s  | Compilers/RewriterWf                                         | 0m00.14s  || +0m00.03s
0m00.15s  | Util/Option                                                  | 0m00.16s  || -0m00.01s
0m00.14s  | Compilers/Named/Compile                                      | 0m00.13s  || +0m00.01s
0m00.13s  | Compilers/Wf                                                 | 0m00.14s  || -0m00.01s
0m00.12s  | Util/Relations                                               | 0m00.12s  || +0m00.00s
0m00.11s  | Compilers/Named/NameUtil                                     | 0m00.12s  || -0m00.00s
0m00.11s  | Compilers/Conversion                                         | 0m00.12s  || -0m00.00s
0m00.11s  | Compilers/Named/IdContext                                    | 0m00.11s  || +0m00.00s
0m00.10s  | Util/Equality                                                | 0m00.10s  || +0m00.00s
0m00.10s  | Util/Prod                                                    | 0m00.10s  || +0m00.00s
0m00.10s  | Util/PointedProp                                             | 0m00.11s  || -0m00.00s
0m00.09s  | Compilers/TypeInversion                                      | 0m00.09s  || +0m00.00s
0m00.09s  | Compilers/Named/MapCast                                      | 0m00.07s  || +0m00.01s
0m00.07s  | Compilers/Syntax                                             | 0m00.05s  || +0m00.02s
0m00.07s  | Compilers/Linearize                                          | 0m00.06s  || +0m00.01s
0m00.06s  | Util/HProp                                                   | 0m00.05s  || +0m00.00s
0m00.06s  | Util/Bool                                                    | 0m00.06s  || +0m00.00s
0m00.06s  | Util/Tower                                                   | 0m00.03s  || +0m00.03s
0m00.06s  | Util/Tactics/BreakMatch                                      | 0m00.03s  || +0m00.03s
0m00.06s  | Util/LetIn                                                   | 0m00.05s  || +0m00.00s
0m00.06s  | Compilers/Inline                                             | 0m00.06s  || +0m00.00s
0m00.06s  | Compilers/RewriterInterp                                     | 0m00.06s  || +0m00.00s
0m00.06s  | Compilers/Named/Syntax                                       | 0m00.06s  || +0m00.00s
0m00.06s  | Compilers/Named/Wf                                           | 0m00.05s  || +0m00.00s
0m00.06s  | Compilers/Named/SmartMap                                     | 0m00.06s  || +0m00.00s
0m00.06s  | Compilers/Eta                                                | 0m00.06s  || +0m00.00s
0m00.06s  | Compilers/FoldTypes                                          | 0m00.06s  || +0m00.00s
0m00.06s  | Compilers/InterpByIso                                        | 0m00.05s  || +0m00.00s
0m00.06s  | Compilers/Named/InterpretToPHOAS                             | 0m00.07s  || -0m00.01s
0m00.05s  | Compilers/Map                                                | 0m00.03s  || +0m00.02s
0m00.05s  | Compilers/Rewriter                                           | 0m00.04s  || +0m00.01s
0m00.04s  | Util/Tactics/DebugPrint                                      | 0m00.04s  || +0m00.00s
0m00.04s  | Util/Isomorphism                                             | 0m00.05s  || -0m00.01s
0m00.04s  | Util/Tactics/Test                                            | 0m00.04s  || +0m00.00s
0m00.04s  | Util/Tactics/ConvoyDestruct                                  | 0m00.03s  || +0m00.01s
0m00.04s  | Util/Tactics/DestructTrivial                                 | 0m00.02s  || +0m00.02s
0m00.04s  | Util/Tactics/ETransitivity                                   | 0m00.03s  || +0m00.01s
0m00.04s  | Util/Curry                                                   | 0m00.03s  || +0m00.01s
0m00.04s  | Util/Sigma/Associativity                                     | 0m00.03s  || +0m00.01s
0m00.04s  | LegacyArithmetic/VerdiTactics                                | 0m00.03s  || +0m00.01s
0m00.04s  | Util/Tactics/Head                                            | 0m00.04s  || +0m00.00s
0m00.04s  | Util/Tactics/Not                                             | 0m00.02s  || +0m00.02s
0m00.04s  | Util/Tactics/UniquePose                                      | 0m00.03s  || +0m00.01s
0m00.04s  | Util/Tactics/DestructHead                                    | 0m00.03s  || +0m00.01s
0m00.04s  | Compilers/TypeUtil                                           | 0m00.03s  || +0m00.01s
0m00.04s  | Util/AutoRewrite                                             | 0m00.04s  || +0m00.00s
0m00.04s  | Compilers/CountLets                                          | 0m00.06s  || -0m00.01s
0m00.04s  | Compilers/Named/Context                                      | 0m00.05s  || -0m00.01s
0m00.03s  | Util/GlobalSettings                                          | 0m00.04s  || -0m00.01s
0m00.03s  | Util/Tactics/Revert                                          | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Tactics/Contains                                        | 0m00.03s  || +0m00.00s
0m00.03s  | Util/IffT                                                    | 0m00.06s  || -0m00.03s
0m00.03s  | Util/Tactics/ClearDuplicates                                 | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/ESpecialize                                     | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/Forward                                         | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/PrintContext                                    | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/SetoidSubst                                     | 0m00.04s  || -0m00.01s
0m00.03s  | Util/Tactics/SideConditionsBeforeToAfter                     | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/SubstEvars                                      | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Tactics/VM                                              | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Sigma/MapProjections                                    | 0m00.03s  || +0m00.00s
0m00.03s  | Util/ChangeInAll                                             | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Sigma/Lift                                              | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Sumbool                                                 | 0m00.09s  || -0m00.06s
0m00.03s  | Util/FixCoqMistakes                                          | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/SpecializeBy                                    | 0m00.04s  || -0m00.01s
0m00.03s  | Util/Tactics/DestructHyps                                    | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Tactics/SplitInContext                                  | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Logic                                                   | 0m00.04s  || -0m00.01s
0m00.03s  | Util/Tactics/RewriteHyp                                      | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/MoveLetIn                                       | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics                                                 | 0m00.04s  || -0m00.01s
0m00.03s  | Compilers/RenameBinders                                      | 0m00.05s  || -0m00.02s
0m00.02s  | Util/Tactics/OnSubterms                                      | 0m00.04s  || -0m00.02s
0m00.02s  | Util/Tactics/GetGoal                                         | 0m00.01s  || +0m00.01s
0m00.02s  | Util/Tactics/ChangeInAll                                     | 0m00.04s  || -0m00.02s
0m00.02s  | Util/Tactics/ClearAll                                        | 0m00.04s  || -0m00.02s
0m00.02s  | Util/Tactics/SetEvars                                        | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Tactics/SimplifyRepeatedIfs                             | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/SubstLet                                        | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/TransparentAssert                               | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/UnifyAbstractReflexivity                        | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Logic/ImplAnd                                           | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Unit                                                    | 0m00.06s  || -0m00.03s
0m00.02s  | Util/Tactics/DoWithHyp                                       | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Notations                                               | 0m00.03s  || -0m00.00s
0m00.01s  | Util/Tactics/EvarExists                                      | 0m00.02s  || -0m00.01s
0m00.01s  | Util/Tactics/SimplifyProjections                             | 0m00.03s  || -0m00.01s

2 files changed, 32 insertions, 39 deletions

diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v
index ff6d3a080..55c73c7fd 100644
--- a/src/Spec/MontgomeryCurve.v
+++ b/src/Spec/MontgomeryCurve.v
@@ -28,7 +28,7 @@ Module M.
                                       | (x, y) => b*y^2 = x^3 + a*x^2 + x
                                       | ∞ => True
                                       end }.
-    Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P.
+    Definition coordinates (P:point) : (F*F + ∞) := let (xyi, _) := P in xyi.
 
     Program Definition zero : point := ∞.
 
@@ -46,29 +46,20 @@ Module M.
               then if Decidable.dec (y1 = - y2)
                    then ∞
                    else let k := (3*x1^2 + 2*a*x1 + 1)/(2*b*y1) in
-                        (b*k^2 - a - x1 - x1, (2*x1 + x1 + a)*k - b*k^3 - y1)
+                        let x := b*k^2 - a - x1 - x2 in
+                        let y := (2*x1 + x2 + a)*k - b*k^3 - y1 in
+                        (x, y)
               else let k := (y2 - y1)/(x2-x1) in
-                   (b*k^2 - a - x1 - x2, (2*x1 + x2 + a)*k - b*k^3 - y1)
+                   let x := b*k^2 - a - x1 - x2 in
+                   let y := (2*x1 + x2 + a)*k - b*k^3 - y1 in
+                   (x, y)
             | ∞, ∞ => ∞
             | ∞, _ => coordinates P2
             | _, ∞ => coordinates P1
             end.
     Next Obligation.
     Proof.
-      repeat match goal with
-             | _ => solve [ trivial ]
-             | _ => progress Tactics.DestructHead.destruct_head' @point
-             | _ => progress Tactics.DestructHead.destruct_head' @prod
-             | _ => progress Tactics.DestructHead.destruct_head' @sum
-             | _ => progress Sum.inversion_sum
-             | _ => progress Prod.inversion_prod
-             | _ => progress Tactics.BreakMatch.break_match_hyps
-             | _ => progress Tactics.BreakMatch.break_match
-             | _ => progress subst
-             | _ => progress cbv [coordinates proj1_sig] in *
-             | |- _ /\ _ => split
-             | |- _ => Field.fsatz
-             end.
+      cbv [coordinates]; BreakMatch.break_match; trivial; Field.fsatz.
     Qed.
   End MontgomeryCurve.
 End M.
diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v
index 226ec6616..fc7c64198 100644
--- a/src/Spec/WeierstrassCurve.v
+++ b/src/Spec/WeierstrassCurve.v
@@ -1,4 +1,4 @@
-Require Crypto.Curves.Weierstrass.Pre.
+Require Crypto.Algebra.Field.
 
 Module W.
   Section WeierstrassCurves.
@@ -29,7 +29,7 @@ Module W.
                               | (x, y) => y^2 = x^3 + a*x + b
                               | ∞ => True
                               end }.
-    Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P.
+    Definition coordinates (P:point) : F*F + ∞ := let (xyi,_) := P in xyi.
 
     Definition eq (P1 P2:point) :=
       match coordinates P1, coordinates P2 with
@@ -43,26 +43,28 @@ Module W.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Notation "2" := (1+1). Local Notation "3" := (1+2). 
 
-    Program Definition add (P1 P2:point) : point  := exist _
-      (match coordinates P1, coordinates P2 return _ with
-       | (x1, y1), (x2, y2) =>
-         if x1 =? x2
-         then
-           if y2 =? -y1
-           then ∞
-           else let k := (3*x1^2+a)/(2*y1) in
-                let x3 := k^2-x1-x1 in
-                let y3 := k*(x1-x3)-y1 in
-                (x3, y3)
-         else let k := (y2-y1)/(x2-x1) in
-              let x3 := k^2-x1-x2 in
-              let y3 := k*(x1-x3)-y1 in
-              (x3, y3)
-       | ∞, ∞ => ∞
-       | ∞, _ => coordinates P2
-       | _, ∞ => coordinates P1
-       end) _.
-    Next Obligation. apply (Pre.add_onCurve _ _ (proj2_sig _) (proj2_sig _)). Qed.
+    Program Definition add (P1 P2:point) : point :=
+      match coordinates P1, coordinates P2 return F*F+∞ with
+      | (x1, y1), (x2, y2) =>
+        if x1 =? x2
+        then
+          if y2 =? -y1
+          then ∞
+          else let k := (3*x1^2+a)/(2*y1) in
+               let x3 := k^2-x1-x2 in
+               let y3 := k*(x1-x3)-y1 in
+               (x3, y3)
+        else let k := (y2-y1)/(x2-x1) in
+             let x3 := k^2-x1-x2 in
+             let y3 := k*(x1-x3)-y1 in
+             (x3, y3)
+      | ∞, ∞ => ∞
+      | ∞, _ => coordinates P2
+      | _, ∞ => coordinates P1
+      end.
+    Next Obligation.
+      cbv [coordinates]; BreakMatch.break_match; trivial; Field.fsatz.
+    Qed.
 
     Fixpoint mul (n:nat) (P : point) : point :=
       match n with