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
...
*
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
*
Add ZUtil lemma
Jason Gross
2016-10-04
*
Add Zmult_lt_compat_r to zarith
Jason Gross
2016-10-04
*
Prevent infinite loops by not dealing with 0 mod _
Jason Gross
2016-10-04
*
Handle 0 mod _ in push_Zmod
Jason Gross
2016-10-04
*
Handle ?x mod ?x in push_Zmod
Jason Gross
2016-10-04
*
Z.ltb_to_lt now also handles eqb
Jason Gross
2016-10-04
*
Work around bug 5107 (broken return inference)
Jason Gross
2016-10-03
*
Work around bug #5112 ([Arguments id /] broken)
Jason Gross
2016-09-30
*
Add Tuple.map
Jason Gross
2016-09-29
*
Revert "Add a locked version of [let] with fewer reductions"
Jason Gross
2016-09-22
*
Revert "Fix LockedLet"
Jason Gross
2016-09-22
*
Fix a typo
Jason Gross
2016-09-22
*
Add a form of Let_In that carries a proof
Jason Gross
2016-09-22
*
alternative signing derivation
Andres Erbsen
2016-09-22
*
Util.LetIn: fix proper instance
Andres Erbsen
2016-09-22
*
Fix LockedLet
Jason Gross
2016-09-22
*
Add a locked version of [let] with fewer reductions
Jason Gross
2016-09-22
*
Reorganization, moving of lemmas to correct files, and 8.4 compatibility
jadep
2016-09-21
*
Change [Let ... in ...] to [dlet ... in ...] (#67)
Jason Gross
2016-09-19
*
Add dec eq for option, list
Jason Gross
2016-09-18
*
Util.Notations: change Let to match slet\
Andres Erbsen
2016-09-18
*
Add reserved notation for Let, change #
Jason Gross
2016-09-17
*
Move side lemmas to appropriate files
jadep
2016-09-17
*
deduplicate Let_In into src/Util/LetIn.v
Andres Erbsen
2016-09-17
*
Add λn reserved notation
Jason Gross
2016-09-16
*
Fix for Coq 8.5
Jason Gross
2016-09-16
*
Add more prop_of_option
Jason Gross
2016-09-16
*
Derive EdDSA.verify from equational specification
Andres Erbsen
2016-09-16
*
IterAssocOp: parameters before arguments
Andres Erbsen
2016-09-16
*
Equality for nat in natutil
Jason Gross
2016-09-16
*
More 8.4 compatibility
jadep
2016-09-14
*
Moved lemmas to ZUtil
jadep
2016-09-13
*
Fully qualify [Require]s
Jason Gross
2016-09-08
*
Work around bug #5073 (lia)
Jason Gross
2016-09-07
*
Add nth_error_In from 8.6
Jason Gross
2016-09-05
*
Add connectives about option pointed_Prop
Jason Gross
2016-09-05
*
Add a coercion [bool >-> option pointed_Prop]
Jason Gross
2016-09-05
[prev]
[next]