index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Util
Commit message (
Expand
)
Author
Age
*
Fix implicit status of curry
Jason Gross
2016-10-27
*
Add curry and uncurry to tuple
Jason Gross
2016-10-27
*
Add tactics to implement better fraction removal
Jason Gross
2016-10-26
*
prove SRepMul admit
Andres Erbsen
2016-10-25
*
Fix for Coq 8.4
Jason Gross
2016-10-24
*
Add more relations about fieldwise
Jason Gross
2016-10-24
*
More 8.4 fixes
Jason Gross
2016-10-23
*
Fix 8.4 build issue
Jason Gross
2016-10-23
*
Prove an admitted NatUtil lemma
Jason Gross
2016-10-23
*
Prove more things in WordUtil
Jason Gross
2016-10-23
*
Fill in some word util admitted lemmas
Jason Gross
2016-10-23
*
Add more specific form of Proper_Let_In_nd_changebody
Jason Gross
2016-10-22
*
Add Bool lemmas about if statements
Jason Gross
2016-10-21
*
Add word64eqb_Zeqb
Jason Gross
2016-10-21
*
Add fold_right_andb_true_iff_fold_right_and_True
Jason Gross
2016-10-19
*
Fix broken [firstorder auto with *] >:-(
Jason Gross
2016-10-19
*
Add Tuple.map2
Jason Gross
2016-10-19
*
Fix for Coq 8.5, 8.5pl1
Jason Gross
2016-10-18
*
Add more simplify lemmas to ZUtil
Jason Gross
2016-10-17
*
Add more simplify lemmas to ZUtil
Jason Gross
2016-10-17
*
Add ZUtil lemma
Jason Gross
2016-10-17
*
refactor scalar multiplication thoery, implement SRepERepMul
Andres Erbsen
2016-10-12
*
integrate bitwise operations
Andres Erbsen
2016-10-12
*
generalize equiv relations in Util.Option and EdDSARepChange
Andres Erbsen
2016-10-12
*
Generalize and simplify cast_word_refl
Jason Gross
2016-10-12
*
word manipulation functions for secret key formatting (#74)
Andres Erbsen
2016-10-12
*
specialize_by: only specialize arguments of type [Prop]
Andres Erbsen
2016-10-10
*
specialize_by: explicitly maintain transparency
Andres Erbsen
2016-10-10
*
Ed25519: add basepoint and prove most EdDSA preconditions
Andres Erbsen
2016-10-10
*
Decidable: add [Z] and [nat] inequalities
Andres Erbsen
2016-10-10
*
Fix compatibility with sigT notation
Jason Gross
2016-10-10
*
Make Ztestbit_full
Jason Gross
2016-10-09
*
Fix Ztestbit_full database
Jason Gross
2016-10-09
*
Fix shiftr_spec_full
Jason Gross
2016-10-09
*
Add more to Ztestbit_full
Jason Gross
2016-10-09
*
Add a Ztestbit_full database
Jason Gross
2016-10-09
*
Stronger Ztestbit, convert_to_ztestbit
Jason Gross
2016-10-07
*
More zsimplify lemmas, stronger Ztestbit
Jason Gross
2016-10-07
*
Add eta_expand to Prod.v
Jason Gross
2016-10-07
*
Weaken hyps of lor_range, add it to zarith
Jason Gross
2016-10-07
*
Moved lemma to ZUtil and added an extra lemma jgross needed
jadep
2016-10-06
*
Add testbit_add_shiftl_full
Jason Gross
2016-10-06
*
Use zutil_arith for side-conditions in testbit
Jason Gross
2016-10-06
*
Add Z.pow_le_mono_{r,l} to zarith
Jason Gross
2016-10-06
*
Add a lemma to Ztestbit about large indices
Jason Gross
2016-10-06
*
More zsimplify lemmas
Jason Gross
2016-10-04
*
Add Zplus_minus to zsimplify
Jason Gross
2016-10-04
*
Weaken hyps of zutil lemma
Jason Gross
2016-10-04
*
Add a variant of add_shift_mod
Jason Gross
2016-10-04
*
Add ZUtil lemma
Jason Gross
2016-10-04
[next]