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
...
*
[cbn] is 8.5 only
Jason Gross
2016-11-11
*
Fix for Coq 8.4
Jason Gross
2016-11-11
*
Fix proofs broken by stronger preconditions
Jason Gross
2016-11-11
*
Most of the admits in Ed25519.v
Rob Sloan
2016-11-11
*
extraction less slow
Andres Erbsen
2016-11-11
*
Add Tuple and HList lemmas
Jason Gross
2016-11-10
*
Work around looping in 8.4
Jason Gross
2016-11-10
*
More proof fixes
Jason Gross
2016-11-10
*
Fix for 8.4
Jason Gross
2016-11-10
*
Minimize diff with master, fix some proofs that were broken
Jason Gross
2016-11-10
*
Hint Rewrite is section-local; move to top-level
Jason Gross
2016-11-10
*
Remove WordizeUtil dependency from WordUtil
Rob Sloan
2016-11-09
*
Merge with master
Rob Sloan
2016-11-09
|
\
|
*
Fix for 8.4
Jason Gross
2016-11-09
|
*
Switch to accurate bounds for lor
Jason Gross
2016-11-09
*
|
Rebase + remove WordizeUtil dependency from Z/Interpretations
Rob Sloan
2016-11-09
|
\
\
|
|
*
Remove last admitted lemma in src/Reflection/Z/Interpretations/Relations.v
Jason Gross
2016-11-09
|
|
/
|
*
Fix bug in 8.4 build
Jason Gross
2016-11-09
|
*
Rewrite cast_word so that it's extracted better
Jason Gross
2016-11-09
|
*
Silence a warning about name collision
Jason Gross
2016-11-09
|
*
Fix bug in 8.4
Jason Gross
2016-11-09
|
*
Split up GF25519Reflective.Common: faster+parallel
Jason Gross
2016-11-09
*
|
Finished WordUtil, word operations in Z/Interpretation
Rob Sloan
2016-11-09
|
*
Add assoc_right
Jason Gross
2016-11-09
|
*
Fix Tuple.map2_S
Jason Gross
2016-11-09
*
|
Not quite done with WordUtil lemmas.
Robert Sloan
2016-11-08
|
\
\
|
|
*
Add Tuple.map2_S
Jason Gross
2016-11-08
|
|
*
Fix for Coq 8.4
Jason Gross
2016-11-08
|
|
*
Fix f_equiv brokenness in 8.4, even faster src/MxDHRepChange.v
Jason Gross
2016-11-08
|
|
*
Faster build of src/MxDHRepChange.v
Jason Gross
2016-11-08
|
|
*
Some fixes for 8.4 differences
Jason Gross
2016-11-08
|
|
*
More progress on src/Reflection/Z/Interpretations/Relations.v
Jason Gross
2016-11-08
|
|
*
Fix precedence issue with 8.4
Jason Gross
2016-11-08
|
|
*
Add map2_map{,_fst,_snd}
Jason Gross
2016-11-08
|
|
*
Add hlist_map
Jason Gross
2016-11-08
|
|
*
Fix 8.4 build ([value] is a constant)
Jason Gross
2016-11-08
|
|
*
Prove things in ModularBaseSystemListZOperationsProofs
Jason Gross
2016-11-08
|
|
/
|
*
Factor related_Z_op (except conditional_sub)
Jason Gross
2016-11-08
|
*
More factoring in related_Z_op
Jason Gross
2016-11-08
|
*
Fix some qualified name issues with previous commit
Jason Gross
2016-11-08
|
*
Add word64ToZ_{neg,cmovne,cmovle,conditional_subtract}
Jason Gross
2016-11-08
|
*
Add HList.const
Jason Gross
2016-11-08
|
*
Rename iffT, add some lemmas about tuple and hlist
Jason Gross
2016-11-08
|
*
Add log2_lt_pow2_alt
Jason Gross
2016-11-08
|
*
Remove lor admit in relations
Jason Gross
2016-11-08
|
*
Work around bug in 8.4
Jason Gross
2016-11-08
|
*
Work around bug 5189 (broken [Hint Resolve ->])
Jason Gross
2016-11-08
|
*
Add Z.lor_nonneg to zarith
Jason Gross
2016-11-08
|
*
Minor refactoring of related_Z_op
Jason Gross
2016-11-07
|
*
Finish related_bounds_t_map1_tuple2
Jason Gross
2016-11-07
[prev]
[next]