aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Add constant-pushing IdWithAlt optimizationGravatar Jason Gross2017-06-14
* Rework and speed up arithmetic simplifier proofsGravatar Jason Gross2017-06-14
* Make rewrite_eta_match_base_type_impl a bit fasterGravatar Jason Gross2017-06-13
* Fix a typoGravatar Jason Gross2017-06-13
* Add rewrite_eta_match_base_type_implGravatar Jason Gross2017-06-13
* Add eta_match_base_type_implGravatar Jason Gross2017-06-13
* Stronger invert_op tacticGravatar Jason Gross2017-06-13
* Fix a major bug in C-notation printingGravatar Jason Gross2017-06-13
* Don't unfold id_with_altGravatar Jason Gross2017-06-13
* Move temporary CNotations importGravatar Jason Gross2017-06-13
* Reify Z.mul_with_split_at_bitwidthGravatar Jason Gross2017-06-13
* Add mul_split_at_bitwidth, define things in terms of thatGravatar Jason Gross2017-06-13
* Update WBW montgomery commentsGravatar Jason Gross2017-06-13
* Add Z.peano_rect_strongGravatar Jason Gross2017-06-13
* Add dec_eq_comparisonGravatar Jason Gross2017-06-13
* Add Z.peano_rectGravatar Jason Gross2017-06-13
* Fill in mul_split to wbw montgomeryGravatar Jason Gross2017-06-13
* Add Z.mul_splitGravatar Jason Gross2017-06-13
* WBW-montgomery: Fill in most context variablesGravatar Jason Gross2017-06-13
* finish computational portions of operations needed for Montgomery, and sketch...Gravatar jadep2017-06-12
* Remove use of id_tuple_with_alt_proofGravatar Jason Gross2017-06-12
* Add a Show to keep track of where we are in karatsubaGravatar Jason Gross2017-06-12
* Handle IdWithAlt in the simplifierGravatar Jason Gross2017-06-12
* Add some more constant notationsGravatar Jason Gross2017-06-12
* WIP on src/Specific/IntegrationTestKaratsubaMul.vGravatar Jason Gross2017-06-12
* Push bounds side conditions through the pipelineGravatar Jason Gross2017-06-12
* Fix zrange notation levelsGravatar Jason Gross2017-06-12
* Add CompileInterpSideConditions.vGravatar Jason Gross2017-06-12
* Add snd_interpf_side_conditions_gen_SomeGravatar Jason Gross2017-06-12
* Add Named.InterpSideConditionsGravatar Jason Gross2017-06-12
* Add Z.InterpSideConditionsGravatar Jason Gross2017-06-12
* Add InterpSideConditionsGravatar Jason Gross2017-06-12
* Have interped_op_side_conditions return a pointed_PropGravatar Jason Gross2017-06-12
* Drop unused [bn] notationGravatar Jason Gross2017-06-12
* Drop some small hyps in light of small_add changeGravatar Jason Gross2017-06-12
* Remove eval_small_bounded_numlimbsGravatar Jason Gross2017-06-12
* Initial stab at id_with_altGravatar Jason Gross2017-06-11
* Add dummy version of IdWithAlt to compilersGravatar Jason Gross2017-06-11
* Factor karatsuba through IdfunWithAlt, add testGravatar Jason Gross2017-06-11
* Add unfold lemmas for id_with_altGravatar Jason Gross2017-06-11
* Add IdfunWithAltGravatar Jason Gross2017-06-11
* Be more forceful about clearing before abstract in glue codeGravatar Jason Gross2017-06-11
* Add script to remake Tactics.v fileGravatar Jason Gross2017-06-11
* Add clearbody_allGravatar Jason Gross2017-06-11
* Fix loop notations, add for loopsGravatar Jason Gross2017-06-11
* Reserve some more notationsGravatar Jason Gross2017-06-11
* cps notations WIP...Gravatar Andres Erbsen2017-06-11
* cps and loop notations WIPGravatar Andres Erbsen2017-06-11
* Finish admits in WordByWord/Proofs.vGravatar Jason Gross2017-06-10
* Add mod_pull_div{,_full}Gravatar Jason Gross2017-06-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 21:53:22 +0000