| Commit message (Expand) | Author | Age |
* | Split up PushButtonSynthesis.v | Jason Gross | 2019-01-18 |
* | Rename Translation.v | jadep | 2019-01-17 |
* | separate toplevel2 into several files; fix up final barrett proof | jadep | 2019-01-17 |
* | Move StringMap into Strings/ | Jason Gross | 2019-01-15 |
* | Add StringMap | Jason Gross | 2019-01-15 |
* | Add String_as_OT | Jason Gross | 2019-01-15 |
* | Autocompute s and c in WBW Montgomery | Jason Gross | 2019-01-14 |
* | remove old pipeline | Andres Erbsen | 2019-01-09 |
* | move src/Experiments/NewPipeline/ to src/ | Andres Erbsen | 2019-01-09 |
* | new pipeline: refactor glue, split into more files | Jason Gross | 2019-01-05 |
* | Add has_body tactic | Jason Gross | 2018-12-21 |
* | Finish rewriter proofs modulo funext | Jason Gross | 2018-12-19 |
* | Add ZRange.OperationBounds | Jason Gross | 2018-12-11 |
* | Add related_sigT_by_eq | Jason Gross | 2018-11-16 |
* | Add PositiveSet Facts | Jason Gross | 2018-10-29 |
* | Add some lemmas about ex, and, eq | Jason Gross | 2018-10-29 |
* | Add CPSId tactics | Jason Gross | 2018-10-28 |
* | Add some equality lemmas about Positive{Map,Set} | Jason Gross | 2018-10-23 |
* | Add interp-correctness condition for rewriter | Jason Gross | 2018-10-11 |
* | Rename [normalize_commutative_identifier] file to match tactic name | Jason Gross | 2018-10-10 |
* | Add [normalize_commutative_identifier] tactic | Jason Gross | 2018-10-10 |
* | Add ListUtil.ForallIn | Jason Gross | 2018-10-09 |
* | Add some lemmas about Bool.reflect | Jason Gross | 2018-09-27 |
* | Add list_elementwise_eqlistA | Jason Gross | 2018-09-14 |
* | Add PrimitiveSigma | Jason Gross | 2018-09-14 |
* | Add a rudimentary arg parse module | Jason Gross | 2018-08-30 |
* | Add src/Util/PER.v | Jason Gross | 2018-08-29 |
* | Minor improvements to various ZUtil things; bounds | Jason Gross | 2018-08-25 |
* | Bump bbv | Jason Gross | 2018-08-24 |
* | Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtil | Jason Gross | 2018-08-23 |
* | Add more operation-specific proofs | Jason Gross | 2018-08-21 |
* | Add the file proving split_bounds correct | Jason Gross | 2018-08-13 |
* | Split up rewrite rules proofs into multiple files | Jason Gross | 2018-08-13 |
* | Start setting up abs-int interp proofs | Jason Gross | 2018-08-06 |
* | Add related_iff_app_curried | Jason Gross | 2018-08-06 |
* | Add GENERATEDIdentifiersWithoutTypesProofs.v | Jason Gross | 2018-08-02 |
* | Integrate Wf and Interp proofs | Jason Gross | 2018-07-30 |
* | Add Wf proofs about MiscCompilerPasses | Jason Gross | 2018-07-26 |
* | Add Wf lemmas about SubstVar | Jason Gross | 2018-07-26 |
* | Add basic wf proofs | Jason Gross | 2018-07-26 |
* | Add some inversion lemmas and tactics | Jason Gross | 2018-07-25 |
* | Montgomery reduction in new pipeline | Jason Gross | 2018-07-21 |
* | Make Z.div_mod_to_quot_rem stronger | Jason Gross | 2018-07-10 |
* | Shuffle some ZUtil lemmas around | Jason Gross | 2018-07-08 |
* | Add ZUtil.Sorting | Jason Gross | 2018-06-29 |
* | Add specialize_all_ways, fix a proof in src/Compilers/Z/ArithmeticSimplifierI... | Jason Gross | 2018-06-26 |
* | New pipeline, split among files | Jason Gross | 2018-06-17 |
* | Add ErrorT monad, and Show class | Jason Gross | 2018-06-15 |
* | Add PrimitiveHList, PrimitiveProd | Jason Gross | 2018-06-13 |
* | Move Option.List.map to OptionList.map to fix name clashes in Tuple | Jason Gross | 2018-06-04 |