aboutsummaryrefslogtreecommitdiff
path: root/src/Fancy
Commit message (Expand)AuthorAge
* update import statementsGravatar jadep2019-04-03
* rename some thingsGravatar jadep2019-04-03
* split up Arithmetic (imports etc. not yet fixed, does not build)Gravatar jadep2019-04-03
* fix montgomeryGravatar jadep2019-03-25
* Get new Barrett proofs to generate Fancy code as beforeGravatar jadep2019-03-25
* finish porting barrett and montgomery code to new glue styleGravatar jadep2019-02-21
* fix cast admits in FancyGravatar jadep2019-02-15
* clean up and factor out cast-admit so that [Print Assumptions] is more fine-g...Gravatar jadep2019-02-08
* cleanupGravatar jadep2019-02-08
* remove some TODOs -- actually, the final proof does not rely on the unused va...Gravatar jadep2019-02-08
* fix Montgomery proof and clean up a littleGravatar jadep2019-02-08
* remove 2: syntax so 8.7 buildsGravatar jadep2019-02-07
* Fix instruction-order admit; still neads cleanupGravatar jadep2019-02-07
* Split up PushButtonSynthesis.vGravatar Jason Gross2019-01-18
* Move print statements to Barrett and Montgomery filesGravatar jadep2019-01-17
* prune dependencies from Barrett256 and Montgomery256Gravatar jadep2019-01-17
* Prune dependencies of Prod.v and fix upGravatar jadep2019-01-17
* Rename Translation.vGravatar jadep2019-01-17
* Prune Translation.v deps and move tactics from other files [WIP]Gravatar jadep2019-01-17
* clean up and prune deps of Spec.vGravatar jadep2019-01-17
* Fix up MontgomeryGravatar jadep2019-01-17
* separate toplevel2 into several files; fix up final barrett proofGravatar jadep2019-01-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 06:49:35 +0000