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 PrimitiveHList, PrimitiveProd
Jason Gross
2018-06-13
*
Move Option.List.map to OptionList.map to fix name clashes in Tuple
Jason Gross
2018-06-04
*
Add Option.List.map
Jason Gross
2018-06-04
*
Move cps notations into a scope
Jason Gross
2018-06-01
*
Add more bind reserved notations
Jason Gross
2018-05-31
*
Move function argument out of fixpoint of List.map2
Jason Gross
2018-05-21
*
Backtrack on moving a notation to Notations.v, to fix conflict
Jason Gross
2018-05-06
*
Fix notations to not conflict with bbv
Jason Gross
2018-05-06
*
More reserved notations
Jason Gross
2018-05-06
*
Add another notation
Jason Gross
2018-05-06
*
Fix a typo in last commit
Jason Gross
2018-05-06
*
Add a reserved notation for #v
Jason Gross
2018-05-06
*
Fix bounds analysis for saturated ops and remove unneeded comment
Jade Philipoom
2018-04-30
*
Util.Loops: remove non-stdlib dependencies
Andres Erbsen
2018-04-26
*
add instructions cc_m, rshi, and sub_with_get_borrow to pipeline in preparati...
Jade Philipoom
2018-04-19
*
Fix a proof
Jason Gross
2018-04-18
*
Change a proof in src/Util/Option
Jason Gross
2018-04-18
*
Merge pull request #335 from mit-plv/cpsloops
Andres Erbsen
2018-04-18
|
\
*
|
add a list lemma
Jade Philipoom
2018-04-11
*
|
add some lemmas aboud div and mod
Jade Philipoom
2018-04-11
*
|
Add new assembly-mimicking operations rshi, cc_m, and cc_l
Jade Philipoom
2018-04-11
*
|
prove stronger bound on quotient error for barrett reduction
Jade Philipoom
2018-04-11
*
|
Update number/string conversions
Jason Gross
2018-04-09
*
|
pass-through after Andres's review in #334
Jade Philipoom
2018-04-03
*
|
move some lemmas to ZUtil/ListUtil
Jade Philipoom
2018-04-03
*
|
move some lemmas/hints to ListUtil
Jade Philipoom
2018-04-03
*
|
Add Zdiv_0_l to zsimplify dbs
Jason Gross
2018-03-27
|
*
move Loops from Experiments to Util
Andres Erbsen
2018-03-27
|
*
remove old loops code
Andres Erbsen
2018-03-27
*
|
Add list_case, a definition for match on list
Jason Gross
2018-03-27
|
/
*
Add another reserved notation for App_fst
Jason Gross
2018-03-21
*
Don't use deprecated compat notations in ZUtil
Jason Gross
2018-03-07
*
git submodule update --remote --recursive
Andres Erbsen
2018-02-24
*
coqprime in COQPATH (closes #269)
Andres Erbsen
2018-02-24
*
Add ZRange.intersection
Jason Gross
2018-02-23
*
Fix a typo
Jason Gross
2018-02-23
*
Add some bounds operations to ZRange
Jason Gross
2018-02-23
*
Add ZRange.opp
Jason Gross
2018-02-23
*
move things from ZUtil.v into Div.v
Jade Philipoom
2018-02-23
*
add three proofs to ZUtil
Jade Philipoom
2018-02-23
*
add two proofs about lists
Jade Philipoom
2018-02-23
*
add proof about Z.equiv_modulo
Jade Philipoom
2018-02-23
*
create rewrite database for saturated operations on Z
Jade Philipoom
2018-02-23
*
Add new modular addition operation on Z
Jade Philipoom
2018-02-23
*
NumTheoryUtil: make coqprime dependencies explicit
Andres Erbsen
2018-02-19
*
Strip the pointed instance names off of the default value in list expansion
Jason Gross
2018-02-18
*
Add expand_lists tactic
Jason Gross
2018-02-18
*
Add pointed types
Jason Gross
2018-02-18
*
Fix a proof for Coq 8.7
Jason Gross
2018-02-17
*
Add lemmas about always_invert_Some and bind
Jason Gross
2018-02-17
[next]