aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* Update build process to use COQPATH & _CoqProjectGravatar Jason Gross2016-02-05
* simple refactor of makefile; commentsGravatar varomodt2016-01-09
* Specific/EdDSA25519: created most of specific instantiation of EdDSA; still m...Gravatar Jade Philipoom2016-01-05
* Code-reviewing EdDSAGravatar Adam Chlipala2015-12-29
* reorganized lemmas; moved several to ListUtil and ZUtil.Gravatar Jade Philipoom2015-11-24
* ModularBaseSystem.carry: implement, state lemmas, some progress on proofsGravatar Andres Erbsen2015-11-17
* Merge remote-tracking branch 'jadep/master'Gravatar Andres Erbsen2015-11-06
|\
* | instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19)Gravatar Andres Erbsen2015-11-06
|/
* Beautified BinGF.splitWordsGravatar Adam Chlipala2015-10-30
* word bound propagation examplesGravatar Andres Erbsen2015-10-30
* BaseSystem to Util.ListUtil: separate out generic list lemmasGravatar Andres Erbsen2015-10-29
* Merge branch 'master' of github.mit.edu:rsloan/fiat-cryptoGravatar Andres Erbsen2015-10-29
|\
| * patches for galoisGravatar Robert Sloan2015-10-27
* | positional number system equivalence transcribed from pencil-and-paper proofs...Gravatar Andres Erbsen2015-10-25
|/
* add morphism-based field implGravatar Robert Sloan2015-10-22
* fix the makefile to not rebuild + module renamingGravatar Robert Sloan2015-10-22
* pull changes from desktopGravatar Robert Sloan2015-10-19
* gfPlus abstractionGravatar Robert Sloan2015-10-16
* make ring decidable + define constantsGravatar Robert Sloan2015-09-19
* makefile dependency orderGravatar Andres Erbsen2015-09-18
* Curves: elliptic curve point format record declarations and some invariantsGravatar Andres Erbsen2015-09-18
* import VerdiTacticsGravatar Andres Erbsen2015-09-17
* redo module structure + init curve25519Gravatar Robert Sloan2015-09-16
* init our centralized repoGravatar Robert Sloan2015-09-10