| 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.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
BoundedWord2
Factor out a tactic and add more examples
BoundedWord2: add test cases
intermediate stage
simple
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
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
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|