Commit message (Collapse) | 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 |
| | | | | | This allows us to make use of nested fixpoints involving map2, because the function argument can be inlined for guard checking now. | ||
* | 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 ↵ | Jade Philipoom | 2018-04-19 |
| | | | | preparation for reifying barrett; tweaked definition of cc_l | ||
* | Fix a proof | Jason Gross | 2018-04-18 |
| | |||
* | Change a proof in src/Util/Option | Jason Gross | 2018-04-18 |
| | | | | | | This was causing issues with bug minimization because some hints seem to follow [Require], not [Import], and so when [eauto] got stronger, this proof was failing. | ||
* | Merge pull request #335 from mit-plv/cpsloops | Andres Erbsen | 2018-04-18 |
|\ | | | | | comprehensive loops framework with complete proof theory | ||
* | | 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 |
| | | | | | | | | To updated version of https://github.com/coq/coq/pull/6597 | ||
* | | 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 |
| | | | | This is required for reification to work, it seems | ||
* | Add expand_lists tactic | Jason Gross | 2018-02-18 |
| | |||
* | Add pointed types | Jason Gross | 2018-02-18 |
| | | | | For filling in default values | ||
* | 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 |
| |