aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/Framework/ArithmeticSynthesis/Base.v
Commit message (Expand)AuthorAge
* Explicitly specify baseGravatar Jason Gross2017-10-18
* Add a few more base thingsGravatar Jason Gross2017-10-18
* Add sz2'_nonzeroGravatar Jason Gross2017-10-18
* Move coef, coef_mod to gallinaGravatar Jason Gross2017-10-18
* Add some more helper lemmas to synthesisGravatar Jason Gross2017-10-18
* Lemmas about wt_genGravatar Jason Gross2017-10-18
* Reorganize the curve-specific synthesis frameworkGravatar Jason Gross2017-10-18