aboutsummaryrefslogtreecommitdiff
path: root/src/Util/AdditionChainExponentiation.v
Commit message (Expand)AuthorAge
* Add a Require Import FunInd (Function isn't loaded by default anymore)Gravatar Pierre Letouzey2017-10-18
* ScalarMult: Z -> G -> G (closes #193)Gravatar Andres Erbsen2017-06-14
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* rename-everythingGravatar Andres Erbsen2017-04-06
* do not use VerdiTactics in files we plan to keepGravatar Andres Erbsen2017-04-06
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* Fully qualify [Require]sGravatar Jason Gross2016-09-08
* Removed lingering SearchAbout.Gravatar jadep2016-08-31
* Updated AdditionChainExponentiation.v such that the exponentiation correctnes...Gravatar jadep2016-08-23
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
* added proofs about addition chain exponentiation for later use in ModularBase...Gravatar jadep2016-07-10