| Commit message (Expand) | Author | Age |
* | Add basic wf proofs | Jason Gross | 2018-07-26 |
* | Actually improve expr.invert_one | Jason Gross | 2018-07-26 |
* | Try again to fix expr inversion | Jason Gross | 2018-07-26 |
* | Improve expr.invert_one (hopefully) | Jason Gross | 2018-07-26 |
* | Add more proper instances | Jason Gross | 2018-07-26 |
* | Add type.eqv for interp equivalence | Jason Gross | 2018-07-26 |
* | Add some inversion lemmas and tactics | Jason Gross | 2018-07-25 |
* | Add invert_LetIn | Jason Gross | 2018-07-25 |
* | Reserve ==, ===, ~= | Jason Gross | 2018-07-25 |
* | Improve rewriter speed | Jason Gross | 2018-07-25 |
* | Add option sequencing/return | Jason Gross | 2018-07-25 |
* | Reserve ;;;, fix level of prefix # to not clash with infix # | Jason Gross | 2018-07-25 |
* | Revert "Improve rewriter speed" | Jason Gross | 2018-07-24 |
* | Improve rewriter speed | Jason Gross | 2018-07-24 |
* | User TIMER_FULL for .ml, .hs, compiled files | Jason Gross | 2018-07-24 |
* | Add ListUtil.{take,drop}_while | Jason Gross | 2018-07-24 |
* | Add git diff for better debugging of C-file issues | Jason Gross | 2018-07-21 |
* | Add some primes to be synthesized | Jason Gross | 2018-07-21 |
* | Montgomery reduction in new pipeline | Jason Gross | 2018-07-21 |
* | Allow building with an external coqprime | Jason Gross | 2018-07-21 |
* | Work around coqprime issues | Jason Gross | 2018-07-21 |
* | Support reification of firstn, skipn | Jason Gross | 2018-07-18 |
* | Make Z.modinv run on wf proofs | Jason Gross | 2018-07-18 |
* | vm_compute in peel_interp_app | Jason Gross | 2018-07-18 |
* | Thunk nat_rect for better perf, list_{rect=>case} | Jason Gross | 2018-07-17 |
* | Handle Z.pow in push_Zmod tactic | Jason Gross | 2018-07-17 |
* | Remove a lemma that's been moved to NatUtil | Jason Gross | 2018-07-17 |
* | Handle Z.pow in {push,pull}_Zmod | Jason Gross | 2018-07-17 |
* | Add minor lemmas to util | Jason Gross | 2018-07-17 |
* | Allow reification of nat_rect (fun _ => _ -> _) | Jason Gross | 2018-07-15 |
* | Add a stronger version of eval_reduce | Jason Gross | 2018-07-14 |
* | Partial adaptation to https://github.com/coq/coq/pull/8063 | Jason Gross | 2018-07-14 |
* | Better error message printing | Jason Gross | 2018-07-12 |
* | Remove useless dependency | Jason Gross | 2018-07-12 |
* | Make Z.div_mod_to_quot_rem stronger | Jason Gross | 2018-07-10 |
* | Bump coqprime | Jason Gross | 2018-07-10 |
* | Allow printing more easily readable code in errors | Jason Gross | 2018-07-09 |
* | Prove that to_bytesmod partitions | Jason Gross | 2018-07-08 |
* | Shuffle some ZUtil lemmas around | Jason Gross | 2018-07-08 |
* | Fix an infinite loop in Z.peel_le | Jason Gross | 2018-07-06 |
* | Remove another thing from the lite target | Jason Gross | 2018-07-03 |
* | Factor eval_reduce_square_exact a bit differently | Jason Gross | 2018-07-03 |
* | Update .gitignore | Jason Gross | 2018-07-03 |
* | Remove nested proofs | Jason Gross | 2018-07-03 |
* | Fix hints, hopefully | Jason Gross | 2018-07-03 |
* | clean | Jason Gross | 2018-07-03 |
* | Finish reduce_square proof | Jason Gross | 2018-07-03 |
* | update c | Jason Gross | 2018-07-03 |
* | Try to fix square again | Jason Gross | 2018-07-03 |
* | update c | Jason Gross | 2018-07-03 |