index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
CompleteEdwardsCurve
/
ExtendedCoordinates.v
Commit message (
Expand
)
Author
Age
*
Fix for 8.6
Jason Gross
2016-11-22
*
Fix for Coq 8.4
Jason Gross
2016-11-21
*
Add add_coordinates_respectful_hetero
Jason Gross
2016-11-17
*
Generalize add_coordinates
Jason Gross
2016-11-17
*
Add add_coordinates_gen
Jason Gross
2016-11-16
*
framework for l_order_B
Andres Erbsen
2016-10-30
*
CompleteEdwardsCurve.ExtendedCoordinates: remove admitted lift_homomorphism l...
Andres Erbsen
2016-10-27
*
fiddle with [rewrite <-!(field_div_definition)], maybe fix build
Andres Erbsen
2016-10-21
*
Edwards.Extended.to_twisted: only one inversion, improve extraction
Andres Erbsen
2016-10-21
*
Be more hesitant to [pose proof E.char_gt_2]
Jason Gross
2016-10-17
*
refactor scalar multiplication thoery, implement SRepERepMul
Andres Erbsen
2016-10-12
*
remove eq_dec from Monoid
Andres Erbsen
2016-08-23
*
Move most notation level declarations into Util
Jason Gross
2016-07-27
*
Make the library 20% faster: [auto with *] is evil
Jason Gross
2016-07-22
*
proved an admit in field homomorphisms that turned out to be unprovable; I ad...
jadep
2016-07-15
*
remove field_algebra
Andres Erbsen
2016-07-11
*
wrap nsatz in Algebra
Andres Erbsen
2016-07-11
*
ExtendedCoordinates: group.
Andres Erbsen
2016-06-24
*
Fix broken notations (hopefully)
Jason Gross
2016-06-22
*
Aggregate all level specifications not in Spec/*
Jason Gross
2016-06-22
*
remove trailing whitespace from src/
Andres Erbsen
2016-06-20
*
move nsatz into tactics directory
Andres Erbsen
2016-06-20
*
tuple tooling
Andres Erbsen
2016-06-20
*
port CompleteEdwardsCurve.ExtendedCoordinates, make [field_algebra] try fewer...
Andres Erbsen
2016-06-18
*
ERep add
Andres Erbsen
2016-05-29
*
before changing SRep from N to F l
Andres Erbsen
2016-05-27
*
slightly nicer edwards curve extended coordinates addition
Andres Erbsen
2016-05-18
*
ed25519: solve elliptic curve math admits
Andres Erbsen
2016-04-25
*
consolidate and rename Edwards curve lemmas
Andres Erbsen
2016-04-25
*
Add a tactic for field inequalities
Jason Gross
2016-04-19
*
Retrieved updated version of Util/IterAssocOp and modified ExtendedCoordinate...
jadep
2016-04-14
*
extended coordinates setoid boilerplate
Andres Erbsen
2016-03-20
*
ModularArithmetic: [field] tactic that respects opacity, prettify ExtendedCoo...
Andres Erbsen
2016-02-28
*
CompleteEdwardsCurve: unifiedAddM1: Closed Under Global Context
Andres Erbsen
2016-02-15
*
document field issue re-appearing
Andres Erbsen
2016-02-12