aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
...
* Change a proof in src/Util/OptionGravatar Jason Gross2018-04-18
* Merge pull request #335 from mit-plv/cpsloopsGravatar Andres Erbsen2018-04-18
|\
* | add a list lemmaGravatar Jade Philipoom2018-04-11
* | add some lemmas aboud div and modGravatar Jade Philipoom2018-04-11
* | Add new assembly-mimicking operations rshi, cc_m, and cc_lGravatar Jade Philipoom2018-04-11
* | prove stronger bound on quotient error for barrett reductionGravatar Jade Philipoom2018-04-11
* | Update number/string conversionsGravatar Jason Gross2018-04-09
* | pass-through after Andres's review in #334Gravatar Jade Philipoom2018-04-03
* | move some lemmas to ZUtil/ListUtilGravatar Jade Philipoom2018-04-03
* | move some lemmas/hints to ListUtilGravatar Jade Philipoom2018-04-03
* | Add Zdiv_0_l to zsimplify dbsGravatar Jason Gross2018-03-27
| * move Loops from Experiments to UtilGravatar Andres Erbsen2018-03-27
| * remove old loops codeGravatar Andres Erbsen2018-03-27
* | Add list_case, a definition for match on listGravatar Jason Gross2018-03-27
|/
* Add another reserved notation for App_fstGravatar Jason Gross2018-03-21
* Don't use deprecated compat notations in ZUtilGravatar Jason Gross2018-03-07
* git submodule update --remote --recursiveGravatar Andres Erbsen2018-02-24
* coqprime in COQPATH (closes #269)Gravatar Andres Erbsen2018-02-24
* Add ZRange.intersectionGravatar Jason Gross2018-02-23
* Fix a typoGravatar Jason Gross2018-02-23
* Add some bounds operations to ZRangeGravatar Jason Gross2018-02-23
* Add ZRange.oppGravatar Jason Gross2018-02-23
* move things from ZUtil.v into Div.vGravatar Jade Philipoom2018-02-23
* add three proofs to ZUtilGravatar Jade Philipoom2018-02-23
* add two proofs about listsGravatar Jade Philipoom2018-02-23
* add proof about Z.equiv_moduloGravatar Jade Philipoom2018-02-23
* create rewrite database for saturated operations on ZGravatar Jade Philipoom2018-02-23
* Add new modular addition operation on ZGravatar Jade Philipoom2018-02-23
* NumTheoryUtil: make coqprime dependencies explicitGravatar Andres Erbsen2018-02-19
* Strip the pointed instance names off of the default value in list expansionGravatar Jason Gross2018-02-18
* Add expand_lists tacticGravatar Jason Gross2018-02-18
* Add pointed typesGravatar Jason Gross2018-02-18
* Fix a proof for Coq 8.7Gravatar Jason Gross2018-02-17
* Add lemmas about always_invert_Some and bindGravatar Jason Gross2018-02-17
* Add always_invert_SomeGravatar Jason Gross2018-02-17
* Add a file to parse taps with Coq notationsGravatar Jason Gross2018-02-14
* Add some string utility functionsGravatar Jason Gross2018-02-13
* Add expand_list_correct to ListUtilGravatar Jason Gross2018-02-12
* Add string conversionsGravatar Jason Gross2018-02-11
* Add notation for option_bindGravatar Jason Gross2018-02-10
* Split off ZRange lemmasGravatar Jason Gross2018-02-10
* Add some ZRange operationsGravatar Jason Gross2018-02-10
* minor updates needed to make it compile with bbvGravatar Samuel Gruetter2018-02-05
* Add better levels / printing for bind notationsGravatar Jason Gross2018-01-16
* Add a comment for why Z.peano_rect_strong exists.Gravatar David Benjamin2018-01-14
* Factor out fsatz lemmasGravatar Jason Gross2018-01-09
* Add @@ infix notationGravatar Jason Gross2018-01-06
* Add some reserved notations for cps stuffGravatar Jason Gross2017-12-27
* Add pow_ceil_mul_nat_divide_nonzeroGravatar Jason Gross2017-12-15
* Add reserved notation for infix @ for applicationGravatar Jason Gross2017-12-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 18:18:58 +0000