index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
Commit message (
Expand
)
Author
Age
*
Don't use UIP in inversion_wff
Jason Gross
2016-12-03
*
Add inversion_wff
Jason Gross
2016-12-03
*
Add WfInversion
Jason Gross
2016-12-03
*
More powerful inversion_option
Jason Gross
2016-12-03
*
Move things to ExprInversion
Jason Gross
2016-12-03
*
Add invert_Var
Jason Gross
2016-12-03
*
Arguments for invert_Op
Jason Gross
2016-12-03
*
Fewer autogenerated names
Jason Gross
2016-12-03
*
Add invert_Op
Jason Gross
2016-12-03
*
Change some default names
Jason Gross
2016-12-03
*
copy_bounds.sh
Jason Gross
2016-12-02
*
Fix looping in Coq 8.4 in ExtendedAddCoordinates.v
Jason Gross
2016-12-02
*
Initial (not fully working) version of MapWithInterpInfo
Jason Gross
2016-12-02
*
Add SmartFlatTypeMapUnInterp
Jason Gross
2016-12-02
*
Add invert_LetIn
Jason Gross
2016-12-02
*
Arguments for invert_Pair
Jason Gross
2016-12-02
*
Add invert_Pair
Jason Gross
2016-12-02
*
Add SmartFlatTypeMapInterp
Jason Gross
2016-12-02
*
SmartFlatTypeMap arguments
Jason Gross
2016-12-02
*
Add SmartFlatTypeMap
Jason Gross
2016-12-02
*
Minor change to inm_op_correct_and_bounded_prefix
Jason Gross
2016-11-25
*
Fix a typo
Jason Gross
2016-11-25
*
Add inm_op_correct_and_bounded_iff_prefix
Jason Gross
2016-11-25
*
Add inm_op_correct_and_bounded
Jason Gross
2016-11-25
*
Also git add in copy_bounds
Jason Gross
2016-11-25
*
uncurry_n_op_fe25519
Jason Gross
2016-11-25
*
Various application lemmas
Jason Gross
2016-11-23
*
More GF25519ReflectiveCommon generalization
Jason Gross
2016-11-22
*
Add tuple lemmas
Jason Gross
2016-11-22
*
Add lemmas about application
Jason Gross
2016-11-22
*
Add impl_under_tower
Jason Gross
2016-11-22
*
Add hlistP
Jason Gross
2016-11-22
*
Add rhlist
Jason Gross
2016-11-22
*
Add interp_all_binders_for'
Jason Gross
2016-11-22
*
Add tower_nd
Jason Gross
2016-11-22
*
Fix for 8.6
Jason Gross
2016-11-22
*
Copy bounds, fix a typo
Jason Gross
2016-11-22
*
Start work on a faster version of GF*Reflective/Common*
Jason Gross
2016-11-21
*
Fix for Coq 8.4
Jason Gross
2016-11-21
*
Fix missing import for List.repeat in 8.4
Jason Gross
2016-11-21
*
Better extraction
Jason Gross
2016-11-17
*
Copy bounds
Jason Gross
2016-11-17
*
Finish proofs about eliminating useless carries
Jason Gross
2016-11-17
*
Add add_coordinates_respectful_hetero
Jason Gross
2016-11-17
*
Remove an admit
Jason Gross
2016-11-17
*
Add fieldwise_map
Jason Gross
2016-11-17
*
Add another admitted lemma
Jason Gross
2016-11-17
*
Generalize add_coordinates
Jason Gross
2016-11-17
*
Add GF25519BoundedExtendedAddCoordinates
Jason Gross
2016-11-17
*
Add src/Specific/GF25519BoundedAddCoordinates.v
Jason Gross
2016-11-17
[next]