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, 2 insertions, 2 deletions

diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v
index c52b4ce87..5733d5cca 100644
--- a/src/Algebra/IntegralDomain.v
+++ b/src/Algebra/IntegralDomain.v
@@ -165,7 +165,7 @@ Module IntegralDomain.
         let x' := constr:(@_LargeCharacteristicReflective.denote R one opp add mul x') in
         change (not (eq x' zero));
         apply (_LargeCharacteristicReflective.is_nonzero_correct(eq:=eq)(zero:=zero) C cg);
-        abstract (vm_cast_no_check (eq_refl true))
+        (vm_cast_no_check (eq_refl true))
       end
     end.
 End IntegralDomain.
diff --git a/src/Algebra/Nsatz.v b/src/Algebra/Nsatz.v
index 2a65e7d82..f1e031d32 100644
--- a/src/Algebra/Nsatz.v
+++ b/src/Algebra/Nsatz.v
@@ -108,7 +108,7 @@ Ltac nsatz_domain_sugar_power domain sugar power :=
     intros _ (* discard [nsatz_compute] output *); intros;
     apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond));
     [ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS]
-    | solve [vm_compute; exact (eq_refl true)] (* exact_no_check (eq_refl true) *)
+    | solve [vm_cast_no_check (eq_refl true)] (* if this fails, the prover returned a bad certificate *)
     | solve [repeat (split; [assumption|]); exact I] ]
   end.