| c59a5ee | kritkorn | 01 April 2017, 18:15:53 UTC | make update-_CoqProject | 01 April 2017, 18:15:53 UTC |
| e95d4a1 | kritkorn | 01 April 2017, 18:13:08 UTC | rebase poly1305 work to master | 01 April 2017, 18:13:08 UTC |
| c7487a5 | Jason Gross | 28 March 2017, 03:08:39 UTC | Add Bounds.dec_eq_interp_flat_type | 28 March 2017, 03:08:39 UTC |
| 676c732 | Andres Erbsen | 26 March 2017, 20:18:36 UTC | crypto-defects.md: add two tweetnacl bugs | 26 March 2017, 20:18:36 UTC |
| 1ebbf1a | jadep | 24 March 2017, 18:40:48 UTC | Added saturated arithmetic file, including [compact] code and proof | 24 March 2017, 18:41:45 UTC |
| de47c4e | jadep | 24 March 2017, 18:38:31 UTC | Add lemmas needed for saturated arithmetic [compact] | 24 March 2017, 18:41:45 UTC |
| 834a48b | Jason Gross | 22 March 2017, 21:27:30 UTC | Fix binder counting in MapCastByDB We were previously counting the names we'd need before linearizing. Oops. | 22 March 2017, 21:27:30 UTC |
| fdff0bf | Jason Gross | 22 March 2017, 21:18:10 UTC | Add aborted CompileProperties This is an attempt to prove that the default counts of let binders are enough. | 22 March 2017, 21:18:10 UTC |
| 4b68b85 | Jason Gross | 22 March 2017, 21:11:59 UTC | Add split_onames_split_names | 22 March 2017, 21:11:59 UTC |
| 210224d | Jason Gross | 22 March 2017, 21:04:27 UTC | Add length_fst_split_names_None_iff | 22 March 2017, 21:04:27 UTC |
| 055d75c | Jason Gross | 22 March 2017, 21:01:31 UTC | Also count lets in operations and pairs | 22 March 2017, 21:01:31 UTC |
| 9c161a6 | Jason Gross | 22 March 2017, 21:01:10 UTC | Add length_fst_split_names_Some_iff | 22 March 2017, 21:01:10 UTC |
| 5b17949 | Jason Gross | 22 March 2017, 19:55:04 UTC | Fix MapCastByDeBruijnInterp | 22 March 2017, 19:55:04 UTC |
| e2e6b8d | Jason Gross | 22 March 2017, 19:40:34 UTC | Prove that mapf_cast gives the correct bounds | 22 March 2017, 19:40:34 UTC |
| bea9b9c | Jason Gross | 22 March 2017, 18:30:43 UTC | Add debug output for success in reifyf | 22 March 2017, 18:30:43 UTC |
| b9cf62e | Jason Gross | 22 March 2017, 16:50:31 UTC | Add cast_back_flat_const | 22 March 2017, 16:50:31 UTC |
| 55ce79c | Jason Gross | 21 March 2017, 21:44:58 UTC | Split off extra power of ltb_to_lt, split_andb This should make the build faster. After | File Name | Before || Change ----------------------------------------------------------------------------------------------------------- 12m23.36s | Total | 19m19.28s || -6m55.91s ----------------------------------------------------------------------------------------------------------- 0m30.37s | Specific/GF25519Bounded | 4m13.77s || -3m43.40s 0m05.10s | Specific/GF25519Reflective/CommonBinOp | 1m03.15s || -0m58.04s 0m04.12s | Specific/GF25519Reflective/CommonUnOp | 0m41.26s || -0m37.14s 0m03.87s | Specific/GF25519Reflective/CommonUnOpWireToFE | 0m36.38s || -0m32.51s 0m02.84s | Specific/GF25519Reflective/CommonUnOpFEToWire | 0m28.09s || -0m25.25s 0m07.65s | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m17.70s || -0m10.04s 0m22.28s | Reflection/Z/Interpretations128/Relations | 0m31.68s || -0m09.39s 0m18.82s | Reflection/Z/Interpretations64/Relations | 0m27.99s || -0m09.16s 0m02.55s | BoundedArithmetic/Double/Proofs/ShiftLeft | 0m06.03s || -0m03.48s 0m06.86s | Reflection/Z/InterpretationsGen | 0m08.87s || -0m02.00s 0m02.55s | BoundedArithmetic/Double/Proofs/ShiftRight | 0m04.69s || -0m02.14s 0m30.47s | ModularArithmetic/ModularBaseSystemProofs | 0m31.67s || -0m01.20s 0m08.77s | Specific/GF25519BoundedCommon | 0m10.43s || -0m01.66s 0m03.07s | ModularArithmetic/ZBoundedZ | 0m04.16s || -0m01.09s 1m29.26s | Test/Curve25519SpecTestVectors | 1m29.49s || -0m00.22s 0m47.87s | Specific/GF25519Reflective/Reified/LadderStep | 0m47.14s || +0m00.72s 0m38.92s | ModularArithmetic/Conversion | 0m39.24s || -0m00.32s 0m36.94s | Spec/Ed25519 | 0m36.07s || +0m00.86s 0m34.26s | Specific/GF25519Reflective/Reified/AddCoordinates | 0m34.09s || +0m00.16s 0m21.21s | ModularArithmetic/Pow2BaseProofs | 0m21.29s || -0m00.07s 0m19.58s | Specific/GF25519 | 0m19.52s || +0m00.05s 0m18.22s | EdDSARepChange | 0m18.44s || -0m00.22s 0m14.71s | Util/ZUtil | 0m14.78s || -0m00.06s 0m14.22s | Reflection/Named/MapCastWf | 0m14.17s || +0m00.05s 0m11.62s | Specific/NewBaseSystemTest | 0m11.50s || +0m00.11s 0m11.13s | Specific/GF25519Reflective/Reified/Mul | 0m11.02s || +0m00.11s 0m11.07s | Experiments/Ed25519 | 0m10.75s || +0m00.32s 0m09.92s | Testbit | 0m09.85s || +0m00.07s 0m08.73s | Reflection/Named/MapCastInterp | 0m08.68s || +0m00.05s 0m08.70s | Assembly/GF25519 | 0m08.70s || +0m00.00s 0m08.67s | ModularArithmetic/Montgomery/ZProofs | 0m09.23s || -0m00.56s 0m08.38s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.50s || -0m00.11s 0m08.18s | BoundedArithmetic/Double/Proofs/Multiply | 0m08.24s || -0m00.06s 0m06.64s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate | 0m06.82s || -0m00.18s 0m06.34s | Specific/GF1305 | 0m06.34s || +0m00.00s 0m06.08s | NewBaseSystem | 0m06.13s || -0m00.04s 0m05.96s | Util/FixedWordSizesEquality | 0m05.87s || +0m00.08s 0m05.72s | Specific/GF25519Reflective/Reified/PreFreeze | 0m05.73s || -0m00.01s 0m05.47s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub | 0m05.42s || +0m00.04s 0m05.22s | Specific/GF25519Reflective/Reified/CarrySub | 0m05.42s || -0m00.20s 0m04.94s | Specific/GF25519Reflective/Reified/CarryAdd | 0m04.90s || +0m00.04s 0m04.91s | Specific/SC25519 | 0m04.95s || -0m00.04s 0m04.88s | ModularArithmetic/ModularBaseSystemListProofs | 0m04.95s || -0m00.07s 0m04.20s | Specific/GF25519Reflective/Common9_4Op | 0m04.10s || +0m00.10s 0m03.89s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.97s || -0m00.08s 0m03.79s | BaseSystemProofs | 0m03.81s || -0m00.02s 0m03.73s | Specific/GF25519Reflective/Reified/CarryOpp | 0m03.80s || -0m00.06s 0m03.51s | Specific/GF25519Reflective/Reified/Sub | 0m03.56s || -0m00.05s 0m03.39s | BoundedArithmetic/InterfaceProofs | 0m03.53s || -0m00.13s 0m03.12s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m03.19s || -0m00.06s 0m02.97s | Specific/GF25519Reflective/Reified/Add | 0m03.16s || -0m00.18s 0m02.94s | ModularArithmetic/ModularArithmeticTheorems | 0m02.86s || +0m00.08s 0m02.78s | Specific/FancyMachine256/Barrett | 0m02.72s || +0m00.05s 0m02.77s | Specific/GF25519ReflectiveAddCoordinates | 0m02.80s || -0m00.02s 0m02.77s | Specific/FancyMachine256/Montgomery | 0m02.86s || -0m00.08s 0m02.75s | Specific/GF25519Reflective/Reified/Pack | 0m02.67s || +0m00.08s 0m02.67s | BoundedArithmetic/Double/Proofs/Decode | 0m02.66s || +0m00.00s 0m02.54s | Specific/GF25519Reflective/Reified/Unpack | 0m02.44s || +0m00.10s 0m02.38s | Specific/GF25519Reflective/Reified/Opp | 0m02.36s || +0m00.02s 0m02.38s | ModularArithmetic/ModularBaseSystemOpt | 0m02.18s || +0m00.19s 0m02.27s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.35s || -0m00.08s 0m02.20s | Reflection/TestCase | 0m02.33s || -0m00.12s 0m02.15s | Specific/GF25519Reflective/Reified/GeModulus | 0m02.05s || +0m00.10s 0m01.98s | Util/WordUtil | 0m02.02s || -0m00.04s 0m01.96s | Assembly/Evaluables | 0m01.96s || +0m00.00s 0m01.88s | Specific/FancyMachine256/Core | 0m01.88s || +0m00.00s 0m01.77s | ModularArithmetic/Montgomery/ZBounded | 0m01.83s || -0m00.06s 0m01.58s | Specific/GF25519Reflective | 0m01.45s || +0m00.13s 0m01.54s | Specific/GF25519Reflective/Common | 0m01.50s || +0m00.04s 0m01.51s | ModularArithmetic/PrimeFieldTheorems | 0m01.44s || +0m00.07s 0m01.50s | Assembly/Compile | 0m01.50s || +0m00.00s 0m01.45s | ModularArithmetic/BarrettReduction/Z | 0m01.48s || -0m00.03s 0m01.28s | Reflection/Z/Syntax/Equality | 0m01.28s || +0m00.00s 0m01.26s | Experiments/Ed25519Extraction | 0m01.28s || -0m00.02s 0m01.24s | Assembly/Conversions | 0m01.12s || +0m00.11s 0m01.22s | Reflection/Z/Interpretations64/RelationsCombinations | 0m01.20s || +0m00.02s 0m01.21s | ModularArithmetic/ExtendedBaseVector | 0m01.15s || +0m00.06s 0m01.21s | Reflection/Z/Interpretations128/RelationsCombinations | 0m01.32s || -0m00.11s 0m01.20s | BaseSystem | 0m01.27s || -0m00.07s 0m01.12s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.03s || +0m00.09s 0m01.10s | Specific/GF25519Reflective/CommonUnOpFEToZ | 0m01.11s || -0m00.01s 0m00.99s | Util/NumTheoryUtil | 0m01.03s || -0m00.04s 0m00.98s | Assembly/HL | 0m00.94s || +0m00.04s 0m00.96s | Assembly/LL | 0m01.00s || -0m00.04s 0m00.94s | Assembly/Pipeline | 0m00.90s || +0m00.03s 0m00.92s | BoundedArithmetic/Double/Proofs/LoadImmediate | 0m00.92s || +0m00.00s 0m00.88s | Specific/GF25519Reflective/Reified | 0m00.72s || +0m00.16s 0m00.83s | Karatsuba | 0m00.94s || -0m00.10s 0m00.82s | Util/IterAssocOp | 0m00.84s || -0m00.02s 0m00.82s | BoundedArithmetic/Double/Proofs/BitwiseOr | 0m00.99s || -0m00.17s 0m00.80s | BoundedArithmetic/X86ToZLikeProofs | 0m00.83s || -0m00.02s 0m00.79s | Assembly/PhoasCommon | 0m00.93s || -0m00.14s 0m00.76s | Specific/GF25519BoundedAddCoordinates | 0m00.79s || -0m00.03s 0m00.75s | ModularArithmetic/ModularBaseSystemList | 0m00.64s || +0m00.10s 0m00.72s | Encoding/ModularWordEncodingTheorems | 0m00.67s || +0m00.04s 0m00.72s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.67s || +0m00.04s 0m00.70s | Reflection/MapCastByDeBruijnInterp | 0m00.64s || +0m00.05s 0m00.68s | ModularArithmetic/ModularBaseSystem | 0m00.67s || +0m00.01s 0m00.67s | BoundedArithmetic/Interface | 0m00.64s || +0m00.03s 0m00.67s | Spec/EdDSA | 0m00.68s || -0m00.01s 0m00.65s | BoundedArithmetic/X86ToZLike | 0m00.55s || +0m00.09s 0m00.63s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.70s || -0m00.06s 0m00.61s | Encoding/ModularWordEncodingPre | 0m00.74s || -0m00.13s 0m00.61s | BoundedArithmetic/Double/Proofs/SelectConditional | 0m00.60s || +0m00.01s 0m00.60s | BoundedArithmetic/Double/Repeated/Proofs/Multiply | 0m00.68s || -0m00.08s 0m00.59s | Spec/ModularWordEncoding | 0m00.58s || +0m00.01s 0m00.56s | Util/NUtil | 0m00.58s || -0m00.01s 0m00.56s | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight | 0m00.48s || +0m00.08s 0m00.54s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.45s || +0m00.09s 0m00.53s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.46s || +0m00.07s 0m00.53s | Reflection/MapCastByDeBruijnWf | 0m00.53s || +0m00.00s 0m00.50s | BoundedArithmetic/ArchitectureToZLike | 0m00.41s || +0m00.09s 0m00.50s | BoundedArithmetic/Double/Repeated/Core | 0m00.47s || +0m00.03s 0m00.50s | BoundedArithmetic/Eta | 0m00.44s || +0m00.06s 0m00.49s | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.52s || -0m00.03s 0m00.49s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.56s || -0m00.07s 0m00.48s | BoundedArithmetic/Double/Core | 0m00.49s || -0m00.01s 0m00.48s | Reflection/Z/Interpretations128 | 0m00.45s || +0m00.02s 0m00.47s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.50s || -0m00.03s 0m00.47s | ModularArithmetic/ModularBaseSystemListZOperationsProofs | 0m00.37s || +0m00.09s 0m00.46s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.38s || +0m00.08s 0m00.46s | BoundedArithmetic/StripCF | 0m00.44s || +0m00.02s 0m00.46s | ModularArithmetic/Pre | 0m00.47s || -0m00.00s 0m00.46s | ModularArithmetic/ZBounded | 0m00.55s || -0m00.09s 0m00.45s | Reflection/Z/Reify | 0m00.48s || -0m00.02s 0m00.44s | ModularArithmetic/Montgomery/Z | 0m00.38s || +0m00.06s 0m00.42s | Reflection/Z/Interpretations64 | 0m00.42s || +0m00.00s 0m00.40s | ModularArithmetic/Pow2Base | 0m00.40s || +0m00.00s 0m00.40s | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic | 0m00.44s || -0m00.03s 0m00.39s | Reflection/Z/Syntax/Util | 0m00.38s || +0m00.01s 0m00.33s | Spec/ModularArithmetic | 0m00.43s || -0m00.09s 0m00.18s | Reflection/CommonSubexpressionElimination | 0m00.15s || +0m00.03s 0m00.05s | Util/Bool | 0m00.04s || +0m00.01s | 21 March 2017, 22:15:19 UTC |
| 26fe989 | Jason Gross | 21 March 2017, 21:32:43 UTC | Remove a line I forgot to remove in the previous commit | 21 March 2017, 21:32:43 UTC |
| 2e3d679 | Jason Gross | 21 March 2017, 21:28:27 UTC | Split off the extra power of rewrite_mod_small into rewrite_mod_mod_small | 21 March 2017, 21:28:27 UTC |
| 279781a | Jason Gross | 21 March 2017, 21:21:44 UTC | Make Z.rewrite_mod_small a bit more powerful Now it can handle things like ((x mod 4) mod 2) when we have (x mod 4 < 2) as a hypothesis. | 21 March 2017, 21:21:44 UTC |
| e717dd5 | Jason Gross | 21 March 2017, 20:30:18 UTC | Make Bool.split_andb a bit more powerful | 21 March 2017, 20:30:18 UTC |
| ec980c5 | Jason Gross | 21 March 2017, 20:27:24 UTC | Make Z.ltb_to_lt a bit stronger Now it works not just at top-level, but also in, e.g., arguments to hypotheses. We had to change some proofs because it no longer moves the hypotheses it changes to the bottom. | 21 March 2017, 20:27:24 UTC |
| d4690fb | Jason Gross | 19 March 2017, 22:54:39 UTC | Add aborted MapCastByDeBruijnWf I'm not sure exactly why the wf proof requires cast_backb in map_cast; it seems to be used as a dumb way of instantiating the context-extension on the input expression tree (since we're only given the context-extension values on the output expression, which has a different type). | 19 March 2017, 22:54:39 UTC |
| 8974f06 | Jason Gross | 19 March 2017, 22:38:47 UTC | Finish MapCastCorrect | 19 March 2017, 22:38:47 UTC |
| 2c24627 | Jason Gross | 19 March 2017, 22:32:33 UTC | Add more to CompileWf | 19 March 2017, 22:32:33 UTC |
| be19ef3 | Jason Gross | 19 March 2017, 22:07:41 UTC | Add MapCastWf | 19 March 2017, 22:07:41 UTC |
| 2fe3e6b | Jason Gross | 19 March 2017, 20:55:45 UTC | Most of the way towards a complete MapCastCorrect | 19 March 2017, 20:55:45 UTC |
| 6a3c0d9 | Jason Gross | 19 March 2017, 20:54:34 UTC | Add Named/PositiveContext/DefaultsProperties.v | 19 March 2017, 20:54:34 UTC |
| 2849fff | Jason Gross | 19 March 2017, 20:49:14 UTC | Add {firstn,skipn}_seq | 19 March 2017, 20:49:14 UTC |
| e8a6a2f | Jason Gross | 19 March 2017, 20:26:45 UTC | Finish CompileInterp proof | 19 March 2017, 20:26:45 UTC |
| 3d24ab3 | Jason Gross | 19 March 2017, 19:47:09 UTC | Split up ContextProperties | 19 March 2017, 19:47:09 UTC |
| ee42b4a | Jason Gross | 19 March 2017, 19:11:37 UTC | Add mname_list_unique_nil | 19 March 2017, 19:11:37 UTC |
| 8675a17 | Jason Gross | 19 March 2017, 19:00:02 UTC | Add more ContextProperties | 19 March 2017, 19:00:02 UTC |
| 5bb615a | Jason Gross | 19 March 2017, 18:36:28 UTC | generalize In_firstn_skipn_split | 19 March 2017, 18:36:28 UTC |
| 2c81383 | Jason Gross | 19 March 2017, 18:20:50 UTC | Add In_firstn_skipn_split | 19 March 2017, 18:20:50 UTC |
| d635e2e | Jason Gross | 19 March 2017, 16:40:33 UTC | Add {m,o,}name_list_unique | 19 March 2017, 16:40:33 UTC |
| 7dcfc8c | Jason Gross | 19 March 2017, 16:09:42 UTC | Add firstn_firstn_min | 19 March 2017, 16:09:42 UTC |
| a1d8da5 | Jason Gross | 17 March 2017, 23:47:09 UTC | Add Addmitted correctness for MapCastByDeBruijn | 19 March 2017, 15:28:41 UTC |
| 100816f | Jason Gross | 19 March 2017, 15:22:59 UTC | Add dummy TWord constructor to syntax type This will allow us to use the same syntax type for the new version of word-size selection without needing to rip out all of the old things. | 19 March 2017, 15:22:59 UTC |
| 1b18ff4 | Jason Gross | 18 March 2017, 22:39:31 UTC | Minor simplification in SmartBound | 18 March 2017, 22:39:31 UTC |
| b3f96bf | Jason Gross | 17 March 2017, 23:47:24 UTC | Add dec_eq_positive | 17 March 2017, 23:47:24 UTC |
| b7e5782 | Jason Gross | 17 March 2017, 23:22:56 UTC | Switch to more robust automation in MapCastInterp | 17 March 2017, 23:22:56 UTC |
| 14d30fc | Jason Gross | 17 March 2017, 23:09:44 UTC | Add default_names_for{,f} | 17 March 2017, 23:10:08 UTC |
| 4988243 | Jason Gross | 17 March 2017, 23:02:50 UTC | Add IdContext | 17 March 2017, 23:02:50 UTC |
| 21eb6f9 | Jason Gross | 17 March 2017, 22:27:48 UTC | Revert "Have cast_op return exprf instead of op" This reverts commit bcfcb5e91011ad0dda68e2b41f871058cf890a3c. Doesn't actually build | 17 March 2017, 22:27:48 UTC |
| bcfcb5e | Jason Gross | 17 March 2017, 22:24:21 UTC | Have cast_op return exprf instead of op cc @andres-erbsen | 17 March 2017, 22:24:52 UTC |
| 24fd7da | Jason Gross | 17 March 2017, 21:46:43 UTC | Add MapCastByDeBruijn on PHOAS syntax | 17 March 2017, 21:46:43 UTC |
| 58dd754 | Jason Gross | 17 March 2017, 18:57:43 UTC | Don't pass a wf proof into InterpToPHOAS Use a fail-value instead. This makes it easier to compose with other transformations. | 17 March 2017, 18:58:17 UTC |
| fbb79ec | Jason Gross | 15 March 2017, 02:25:04 UTC | Add aborted in-process compile-{wf,interp} proofs | 17 March 2017, 18:38:07 UTC |
| 35b540e | Jason Gross | 09 March 2017, 04:56:48 UTC | Add a Named version of MapCast Based on Andres' work towards #123. | 17 March 2017, 18:27:19 UTC |
| fe6e81c | Andres Erbsen | 17 March 2017, 01:18:03 UTC | Update crypto-defects.md https://blogs.adobe.com/security/2017/03/critical-vulnerability-uncovered-in-json-encryption.html | 17 March 2017, 01:18:03 UTC |
| 8ef051f | Jason Gross | 16 March 2017, 00:05:35 UTC | [travis] Only build the lite target on Coq 8.5 This closes #122 | 16 March 2017, 21:27:51 UTC |
| d826ef0 | Jason Gross | 15 March 2017, 17:36:43 UTC | Add a "lite" target This builds everything in the default target except WeierstrassCurveTheorems.vo, which, I believe, is the slowest file. This closes #129. | 15 March 2017, 17:36:43 UTC |
| 2c2ac41 | Jason Gross | 15 March 2017, 02:33:44 UTC | Fix a name clash | 15 March 2017, 02:33:44 UTC |
| 44b5603 | Jason Gross | 15 March 2017, 02:17:11 UTC | Add split_{m,o,}names_firstn_skipn and co. | 15 March 2017, 02:17:11 UTC |
| 13441cb | Jason Gross | 15 March 2017, 01:59:44 UTC | Add firstn_skipn | 15 March 2017, 01:59:44 UTC |
| dbcae76 | Jason Gross | 15 March 2017, 01:59:35 UTC | Add split_prod | 15 March 2017, 01:59:35 UTC |
| 5cefabf | Jason Gross | 15 March 2017, 01:19:05 UTC | Add NameUtilProperties | 15 March 2017, 01:19:05 UTC |
| b2e1bc6 | Jason Gross | 15 March 2017, 01:09:16 UTC | Add skipn_skipn | 15 March 2017, 01:09:16 UTC |
| 035b162 | Jason Gross | 14 March 2017, 21:20:16 UTC | Add InterpretToPHOASInterp | 14 March 2017, 21:20:16 UTC |
| 1cd8fd2 | Jason Gross | 14 March 2017, 20:10:14 UTC | Add Wf_InterpToPHOAS | 14 March 2017, 20:10:14 UTC |
| 4bac3c4 | Jason Gross | 14 March 2017, 19:15:22 UTC | Remove useless hyps | 14 March 2017, 19:15:22 UTC |
| bf3783d | Jason Gross | 14 March 2017, 19:13:45 UTC | Add InterpretToPHOAS | 14 March 2017, 19:13:45 UTC |
| fa089c9 | Jason Gross | 14 March 2017, 18:17:08 UTC | Move find_if_eq to Decidable.v, use Decidable in Named | 14 March 2017, 18:17:08 UTC |
| 7a3740e | Jason Gross | 14 March 2017, 18:05:55 UTC | Add ContextProperties | 14 March 2017, 18:05:55 UTC |
| 144354f | Jason Gross | 14 March 2017, 17:22:27 UTC | Remove useless imports | 14 March 2017, 17:22:27 UTC |
| 29583c6 | Jason Gross | 14 March 2017, 17:20:31 UTC | Move ContextOk to ContextDefinitions | 14 March 2017, 17:20:31 UTC |
| 8c8a223 | Jason Gross | 14 March 2017, 17:16:25 UTC | Add lemma about wff and interpf of Named | 14 March 2017, 17:16:25 UTC |
| feb04cf | Jason Gross | 14 March 2017, 16:26:19 UTC | Add faster versions of destruct_head_* Sometimes, it's a performance bottleneck | 14 March 2017, 16:26:19 UTC |
| b5abd90 | Jason Gross | 10 March 2017, 16:12:00 UTC | Fix more unfolding | 10 March 2017, 16:12:00 UTC |
| 2b3c61f | Jason Gross | 10 March 2017, 16:06:52 UTC | Fix more unfolding that shouldn't happen | 10 March 2017, 16:06:52 UTC |
| e4921f4 | Jason Gross | 10 March 2017, 16:04:25 UTC | Make sure interp_flat_type isn't unfolded in SmartMap | 10 March 2017, 16:04:25 UTC |
| 00b3ebb | Jason Gross | 09 March 2017, 04:54:12 UTC | Add better SmartFlatTypeMapInterp2 | 09 March 2017, 04:54:12 UTC |
| af588d2 | Jason Gross | 09 March 2017, 04:37:12 UTC | Remove interp_genf from Named/Syntax | 09 March 2017, 04:37:12 UTC |
| caec53c | Jason Gross | 08 March 2017, 19:57:14 UTC | Remove stuff from Reflection/Named/Syntax | 08 March 2017, 22:07:53 UTC |
| 9af802f | Jason Gross | 08 March 2017, 19:56:25 UTC | Add FMapContext, PositiveContext Also copy some definitions from Syntax out of it, in prep for removing them | 08 March 2017, 19:56:25 UTC |
| 122e6f6 | Jason Gross | 06 March 2017, 17:39:22 UTC | Remove display .vo from default target | 07 March 2017, 04:48:15 UTC |
| 04f2699 | jadep | 06 March 2017, 19:36:47 UTC | Fixes #127 | 06 March 2017, 19:36:51 UTC |
| efb6df3 | Jason Gross | 06 March 2017, 17:40:10 UTC | JavaDisplay depends on JavaNotations, not CNotations | 06 March 2017, 17:40:25 UTC |
| 8e212b2 | jadep | 04 March 2017, 20:36:42 UTC | Remove assert_preconditions; prove ring-ness of basesystem operations for base 2^25.5 | 04 March 2017, 20:36:42 UTC |
| 3983d87 | jadep | 04 March 2017, 17:16:09 UTC | Separated out specific test cases for new base system | 04 March 2017, 17:16:09 UTC |
| c00de42 | jadep | 02 March 2017, 19:05:38 UTC | Fixed admit left from fsatz port | 02 March 2017, 19:05:38 UTC |
| 0ab98d3 | Andres Erbsen | 02 March 2017, 15:58:28 UTC | make 8.5 happy | 02 March 2017, 18:37:14 UTC |
| 7f0ba34 | Andres Erbsen | 02 March 2017, 13:18:01 UTC | fixup NewBasesystem | 02 March 2017, 18:37:14 UTC |
| 90b9f8d | Andres Erbsen | 02 March 2017, 12:20:41 UTC | remove dangling file... | 02 March 2017, 18:37:14 UTC |
| 59662e3 | Andres Erbsen | 01 March 2017, 17:06:21 UTC | remove dangling file that gives a warning | 02 March 2017, 18:37:14 UTC |
| cffd104 | Andres Erbsen | 01 March 2017, 16:14:11 UTC | remove undeclared lines from Ed25519Extraction.v | 02 March 2017, 18:37:14 UTC |
| 83be64b | Andres Erbsen | 01 March 2017, 04:11:05 UTC | move large non-building chunks of Ed25519.v | 02 March 2017, 18:37:14 UTC |
| c55c410 | Andres Erbsen | 28 February 2017, 15:40:56 UTC | deleted src/Specific/GF25519ExtendedAddCoordinates.v | 02 March 2017, 18:37:14 UTC |
| 153acc4 | Andres Erbsen | 28 February 2017, 14:41:11 UTC | fix src/Specific/GF25519Reflective/Reified/AddCoordinates.v | 02 March 2017, 18:37:14 UTC |
| 4b8a44a | Andres Erbsen | 23 February 2017, 17:25:36 UTC | remove PointEncoding | 02 March 2017, 18:37:14 UTC |
| 996734b | Andres Erbsen | 23 February 2017, 17:23:28 UTC | CompleteEdwardsCurveTheorems: point compression | 02 March 2017, 18:37:14 UTC |
| 4016108 | Andres Erbsen | 22 February 2017, 23:32:19 UTC | PrimeFieldTheorems: inv for isomorphic fields | 02 March 2017, 18:37:14 UTC |
| 2a321d8 | Andres Erbsen | 22 February 2017, 19:11:41 UTC | use [positive] for [F] modulus, char_ge_C instead of char_gt_C | 02 March 2017, 18:37:14 UTC |
| f5c6a57 | Andres Erbsen | 21 February 2017, 23:01:18 UTC | rewrite ExtendedCoordinates, fix Ed25519 | 02 March 2017, 18:37:14 UTC |
| c1c764e | Andres Erbsen | 20 February 2017, 18:42:19 UTC | edwards curves over isomorphic fields | 02 March 2017, 18:37:14 UTC |
| a3e42ef | Andres Erbsen | 20 February 2017, 18:42:00 UTC | src/Tactics/Algebra_syntax/Nsatz.v: power 1 only | 02 March 2017, 18:37:14 UTC |
| af51418 | Andres Erbsen | 17 February 2017, 04:56:47 UTC | WIP | 02 March 2017, 18:37:14 UTC |
| 0a6e65e | Andres Erbsen | 15 February 2017, 18:18:40 UTC | address some code review comments | 02 March 2017, 18:37:14 UTC |
| 0a9ea9d | Andres Erbsen | 13 February 2017, 20:27:19 UTC | Weierstrass curve is a group | 02 March 2017, 18:37:14 UTC |
