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
*
Add Z.mod_mod to zsimplify
Jason Gross
2016-07-28
*
Move most notation level declarations into Util
Jason Gross
2016-07-27
*
Restore functionality of Z.simplify_fractions_le
Jason Gross
2016-07-27
*
Make Z.pre_reorder_fractions / Z.simplify_fractions_le not loop
Jason Gross
2016-07-27
*
Add another ZUtil lemma
Jason Gross
2016-07-26
*
Fix 8.4 build.
jadep
2016-07-25
*
Merge branch 'master' of github.com:mit-plv/fiat-crypto
jadep
2016-07-25
|
\
*
|
A couple new util lemmas
jadep
2016-07-25
|
*
More Zpow in ZUtil
Jason Gross
2016-07-22
|
*
More ZUtil
Jason Gross
2016-07-22
|
*
Add reverse_nondep and ring_simplify_subterms_in_all tactics
Jason Gross
2016-07-22
|
*
More ZUtil lemmas
Jason Gross
2016-07-22
|
*
Revert "Revert "Add more ZUtil automation""
Jason Gross
2016-07-22
|
*
Make the library 20% faster: [auto with *] is evil
Jason Gross
2016-07-22
|
*
Revert "Add more ZUtil automation"
Jason Gross
2016-07-22
|
*
Add more ZUtil automation
Jason Gross
2016-07-22
|
*
Add ring_simplify_subterms
Jason Gross
2016-07-22
|
*
Generalize div_sub_small a bit
Jason Gross
2016-07-22
|
/
*
Add another lemma to zarith
Jason Gross
2016-07-21
*
Add another ZUtil lemma
Jason Gross
2016-07-21
*
Another ZUtil lemma
Jason Gross
2016-07-21
*
Fix broken proofs
Jason Gross
2016-07-21
*
Add more ZUtil
Jason Gross
2016-07-21
*
More ZUtil helper lemmas
Jason Gross
2016-07-21
*
Add more ZUtil lemmas
Jason Gross
2016-07-21
*
Add ZUtil lemmas
Jason Gross
2016-07-21
*
Add Z.lt_le_incl to zarith
Jason Gross
2016-07-20
*
Add another lemma about +, <= to arith
Jason Gross
2016-07-20
*
Add a distr_length database
Jason Gross
2016-07-19
*
Remove stuff from PseudoMersenneBaseParamProofs.v
Jason Gross
2016-07-19
*
Add a lemma about sum_firstn
Jason Gross
2016-07-18
*
Add a ListUtil lemma
Jason Gross
2016-07-18
*
Fix for Coq 8.4 (missing lemmas)
Jason Gross
2016-07-18
*
Fix for Coq 8.4 (omega used to be weaker)
Jason Gross
2016-07-18
*
Add more natsimplify le_dec lemmas
Jason Gross
2016-07-18
*
Add more NatUtil lemmas
Jason Gross
2016-07-18
*
Add natsimplify lemmas about eq_nat_dec
Jason Gross
2016-07-18
*
Fix some typos in the previous commit
Jason Gross
2016-07-18
*
Add some lemmas about nth_default in bounds
Jason Gross
2016-07-18
*
Move some definitions to Pow2Base (#24)
Jason Gross
2016-07-18
*
ported IterAssocOp to use monoid rather than a billion context variables that...
jadep
2016-07-18
*
Added lemmas to ZUtil and NatUtil (for Testbit)
jadep
2016-07-18
*
tuple: applying functions to tuples of arbitrary length
Andres Erbsen
2016-07-12
*
Merge of fixedlength and master
jadep
2016-07-11
|
\
|
*
wrap nsatz in Algebra
Andres Erbsen
2016-07-11
|
*
[congruence] is more powerful in 8.5 than in 8.4
Andres Erbsen
2016-07-11
|
*
merge
jadep
2016-07-10
|
|
\
|
*
|
added proofs about addition chain exponentiation for later use in ModularBase...
jadep
2016-07-10
|
|
*
Fix ListUtil for Coq 8.4
Jason Gross
2016-07-10
|
|
*
Update ListUtil
Jason Gross
2016-07-08
[next]