| Commit message (Expand) | Author | Age |
* | 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 |
* | make update-_CoqProject | Jason Gross | 2018-05-05 |
* | Merge pull request #335 from mit-plv/cpsloops | Andres Erbsen | 2018-04-18 |
|\ |
|
* | | Add new assembly-mimicking operations rshi, cc_m, and cc_l | Jade Philipoom | 2018-04-11 |
* | | Update number/string conversions | Jason Gross | 2018-04-09 |
| * | move Loops from Experiments to Util | Andres Erbsen | 2018-03-27 |
| * | remove old loops code | Andres Erbsen | 2018-03-27 |
|/ |
|
* | Add Algebra.SubsetoidRing | Jason Gross | 2018-03-12 |
* | make update-_CoqProject | Jason Gross | 2018-03-10 |
* | Prove another Barrett reduction variant. | David Benjamin | 2018-03-09 |