| Commit message (Collapse) | Author | Age |
|
|
|
| |
ExtendedCoordinates, outline Edwards curve associativity
|
| |
|
| |
|
| |
|
|
|
|
| |
It still builds with 8.4
|
|
|
|
| |
Also move a definition about words, with a TODO about location, into WordUtil.
|
|\ |
|
| | |
|
| |
| |
| |
| |
| | |
Ambiguous imports, oh joy! (Coqprime failed to build when Bedrock was in
COQPATH.)
|
|/
|
|
|
|
| |
It is used on smithers to remove .vo files which are older than relevant
Bedrock .vo files. This prevents version mismatches when updating Bedrock on
smithers.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
CompleteEdwardsCurve, where the precondition is not in scope.
|
|
|
|
| |
imports of PointFormats and Galois things)
|
| |
|
| |
|
| |
|
| |
|
|\ |
|
| |
| |
| |
| | |
the commit looks huge)
|
| | |
|
| |
| |
| |
| | |
PrimeFieldTheorems
|
| | |
|
| | |
|
|/ |
|
|\ |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
positivity/nonnegativity in Z
|
| | |
|
|/ |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
Closed Under Global Context
|
|\ |
|
| | |
|
| | |
|
| |\
| |/
|/| |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|