Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add constr_fail and constr_fail_with | Jason Gross | 2019-03-31 |
| | | | | | | | | | | | | | Rather than taking the convention that failures during constr construction emit a type error from `I : I` with the actual error message `idtac`d above them (because Coq has no way to emit multiple things on stderr), we instead factor everything through a new `constr_fail` or `constr_fail_with msg_tac`, which emit more helpful messages instructing the user to look in `*coq*` or to use `Fail`/`try` to see the more informative error message. When we can make our own version that does both `idtac` and `fail` (c.f. https://github.com/coq/coq/issues/3913), then we can do something a bit more sane, hopefully. | ||
* | Fix issue with previous commit | Jason Gross | 2019-03-08 |
| | |||
* | Add some eq list_rect lemmas to ListUtil | Jason Gross | 2019-03-08 |
| | |||
* | Add some eq lemmas to ListUtil | Jason Gross | 2019-03-07 |
| | |||
* | Add some Proper lemmas to ListUtil | Jason Gross | 2019-03-07 |
| | |||
* | Add remove_duplicates | Jason Gross | 2019-01-24 |
| | |||
* | prove [eval_conditional_sub] | jadep | 2018-12-21 |
| | |||
* | Add Forall2_update_nth | Jason Gross | 2018-12-06 |
| | |||
* | Remove ListUtil.List.repeat | Jason Gross | 2018-12-04 |
| | | | | | We are no longer checking against Coq 8.5, and it's simpler to not have two versions of `List.repeat` floating around. | ||
* | Add map_repeat, map_const | Jason Gross | 2018-11-11 |
| | |||
* | Add some natutil and listutil lemmas | Jason Gross | 2018-10-10 |
| | |||
* | Add map_update_nth_ext | Jason Gross | 2018-10-09 |
| | |||
* | Add some util lemmas | Jason Gross | 2018-08-13 |
| | |||
* | Add ListUtil.map_nth_default_seq | Jason Gross | 2018-08-10 |
| | |||
* | Add ListUtil.{combine_repeat,combine_rev_rev_samelength} | Jason Gross | 2018-08-09 |
| | |||
* | Add nth_error_combine | Jason Gross | 2018-08-01 |
| | |||
* | Add more proper instances | Jason Gross | 2018-07-26 |
| | |||
* | Add ListUtil.{take,drop}_while | Jason Gross | 2018-07-24 |
| | |||
* | Add minor lemmas to util | Jason Gross | 2018-07-17 |
| | |||
* | Add ZUtil, list lemmas | Jason Gross | 2018-07-02 |
| | |||
* | Fix a notation issue in previous commit | Jason Gross | 2018-07-02 |
| | |||
* | Add more ListUtil proofs | Jason Gross | 2018-07-02 |
| | |||
* | Add some list lemmas | Jason Gross | 2018-07-02 |
| | |||
* | Add useful list lemmas | Jason Gross | 2018-06-29 |
| | |||
* | Add list_beq | Jason Gross | 2018-06-22 |
| | |||
* | Add seq_add, seq_len_0 | Jason Gross | 2018-06-19 |
| | |||
* | 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. | ||
* | add a list lemma | Jade Philipoom | 2018-04-11 |
| | |||
* | 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 list_case, a definition for match on list | Jason Gross | 2018-03-27 |
| | |||
* | add two proofs about lists | Jade Philipoom | 2018-02-23 |
| | |||
* | 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 expand_list_correct to ListUtil | Jason Gross | 2018-02-12 |
| | |||
* | Generalize Forall2_forall_iff | Jason Gross | 2017-11-09 |
| | |||
* | src/Demo.v: a 200-line introduction to BaseSystem ideas | Andres Erbsen | 2017-06-21 |
| | |||
* | Don't rely on autogenerated names | Jason Gross | 2017-06-05 |
| | | | | | | This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch). | ||
* | s/appcontext/context/ | Jason Gross | 2017-05-11 |
| | | | | They mean the same thing since 8.5, and appcontext is deprecated. | ||
* | do not use VerdiTactics in files we plan to keep | Andres Erbsen | 2017-04-06 |
| | |||
* | Add [Proof using] to most proofs | Jason Gross | 2017-04-04 |
| | | | | | | | | This closes #146 and makes `make quick` faster. The changes were generated by adding [Global Set Suggest Proof Using.] to GlobalSettings.v, and then following [the instructions for a script I wrote](https://github.com/JasonGross/coq-tools#proof-using-helper). | ||
* | Add lemmas needed for saturated arithmetic [compact] | jadep | 2017-03-24 |
| | |||
* | Add {firstn,skipn}_seq | Jason Gross | 2017-03-19 |
| | |||
* | generalize In_firstn_skipn_split | Jason Gross | 2017-03-19 |
| | |||
* | Add In_firstn_skipn_split | Jason Gross | 2017-03-19 |
| | |||
* | Add firstn_firstn_min | Jason Gross | 2017-03-19 |
| | |||
* | Fix a name clash | Jason Gross | 2017-03-14 |
| | |||
* | Add firstn_skipn | Jason Gross | 2017-03-14 |
| | |||
* | Add skipn_skipn | Jason Gross | 2017-03-14 |
| |