aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Support reification of firstn, skipnGravatar Jason Gross2018-07-18
* Make Z.modinv run on wf proofsGravatar Jason Gross2018-07-18
* vm_compute in peel_interp_appGravatar Jason Gross2018-07-18
* Thunk nat_rect for better perf, list_{rect=>case}Gravatar Jason Gross2018-07-17
* Handle Z.pow in push_Zmod tacticGravatar Jason Gross2018-07-17
* Remove a lemma that's been moved to NatUtilGravatar Jason Gross2018-07-17
* Handle Z.pow in {push,pull}_ZmodGravatar Jason Gross2018-07-17
* Add minor lemmas to utilGravatar Jason Gross2018-07-17
* Allow reification of nat_rect (fun _ => _ -> _)Gravatar Jason Gross2018-07-15
* Add a stronger version of eval_reduceGravatar Jason Gross2018-07-14
* Partial adaptation to https://github.com/coq/coq/pull/8063Gravatar Jason Gross2018-07-14
* Better error message printingGravatar Jason Gross2018-07-12
* Remove useless dependencyGravatar Jason Gross2018-07-12
* Make Z.div_mod_to_quot_rem strongerGravatar Jason Gross2018-07-10
* Allow printing more easily readable code in errorsGravatar Jason Gross2018-07-09
* Prove that to_bytesmod partitionsGravatar Jason Gross2018-07-08
* Shuffle some ZUtil lemmas aroundGravatar Jason Gross2018-07-08
* Fix an infinite loop in Z.peel_leGravatar Jason Gross2018-07-06
* Factor eval_reduce_square_exact a bit differentlyGravatar Jason Gross2018-07-03
* Remove nested proofsGravatar Jason Gross2018-07-03
* Fix hints, hopefullyGravatar Jason Gross2018-07-03
* cleanGravatar Jason Gross2018-07-03
* Finish reduce_square proofGravatar Jason Gross2018-07-03
* Try to fix square againGravatar Jason Gross2018-07-03
* Fix a typo, start on proofGravatar Jason Gross2018-07-03
* Fix a reification issueGravatar Jason Gross2018-07-03
* Try a different reduce_squareGravatar Jason Gross2018-07-03
* WIP better squareGravatar Jason Gross2018-07-03
* Fix missing argGravatar Jason Gross2018-07-03
* Add missing spaceGravatar Jason Gross2018-07-03
* Add support for annotating generated C functions with commentsGravatar Jason Gross2018-07-03
* Synthesize selectznzGravatar Jason Gross2018-07-03
* Correctly reify match on prodGravatar Jason Gross2018-07-03
* Add selectGravatar Jason Gross2018-07-03
* Comment out some code that's too slowGravatar Jason Gross2018-07-03
* Allow passing functions to synthesize on the command line, and scmul for 25519Gravatar Jason Gross2018-07-03
* Pull out *2 in square, don't turn *2 into <<1Gravatar Jason Gross2018-07-03
* No subst01 in mulmodGravatar Jason Gross2018-07-03
* Start with a better template for carry_squareGravatar Jason Gross2018-07-03
* Don't subst01 in squareGravatar Jason Gross2018-07-03
* synthesize squareGravatar Jason Gross2018-07-03
* static in cGravatar Jason Gross2018-07-03
* static voidGravatar Jason Gross2018-07-03
* WIPGravatar Jason Gross2018-07-03
* Add ZUtil, list lemmasGravatar Jason Gross2018-07-02
* Fix a notation issue in previous commitGravatar Jason Gross2018-07-02
* Add more ListUtil proofsGravatar Jason Gross2018-07-02
* Add some list lemmasGravatar Jason Gross2018-07-02
* Make all parameters implicitGravatar Jasper Hugunin2018-07-02
* Prefer relations of the form [eq ==> eq ==> ... ==> eq] in setoidsGravatar Jason Gross2018-07-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 21:22:43 +0000