aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Add seq_add, seq_len_0Gravatar Jason Gross2018-06-19
* Add ShowLinesGravatar Jason Gross2018-06-17
* Reserve a notatoin for ;;Gravatar Jason Gross2018-06-16
* Add zrange equalityGravatar Jason Gross2018-06-15
* Add ErrorT monad, and Show classGravatar Jason Gross2018-06-15
* Add decimal_string_of_ZGravatar Jason Gross2018-06-15
* Add some lemmas and defs to ListUtil.FoldBoolGravatar Jason Gross2018-06-14
* Set universe polymorphism in CPSNotationsGravatar Jason Gross2018-06-14
* Add notations for cpsbind, cps_option_bindGravatar Jason Gross2018-06-14
* Actually use primitive projections in PrimitiveHListGravatar Jason Gross2018-06-13
* Minor refactoringGravatar Jason Gross2018-06-13
* Add PrimitiveHList, PrimitiveProdGravatar Jason Gross2018-06-13
* Move Option.List.map to OptionList.map to fix name clashes in TupleGravatar Jason Gross2018-06-04
* Add Option.List.mapGravatar Jason Gross2018-06-04
* Move cps notations into a scopeGravatar Jason Gross2018-06-01
* Add more bind reserved notationsGravatar Jason Gross2018-05-31
* Move function argument out of fixpoint of List.map2Gravatar Jason Gross2018-05-21
* Backtrack on moving a notation to Notations.v, to fix conflictGravatar Jason Gross2018-05-06
* Fix notations to not conflict with bbvGravatar Jason Gross2018-05-06
* More reserved notationsGravatar Jason Gross2018-05-06
* Add another notationGravatar Jason Gross2018-05-06
* Fix a typo in last commitGravatar Jason Gross2018-05-06
* Add a reserved notation for #vGravatar Jason Gross2018-05-06
* Fix bounds analysis for saturated ops and remove unneeded commentGravatar Jade Philipoom2018-04-30
* Util.Loops: remove non-stdlib dependenciesGravatar Andres Erbsen2018-04-26
* add instructions cc_m, rshi, and sub_with_get_borrow to pipeline in preparati...Gravatar Jade Philipoom2018-04-19
* Fix a proofGravatar Jason Gross2018-04-18
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 16:37:39 +0000