Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | prove [eval_conditional_sub] | 2018-12-21 | |
| | |||
* | Add Forall2_update_nth | 2018-12-06 | |
| | |||
* | Remove ListUtil.List.repeat | 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 | 2018-11-11 | |
| | |||
* | Add some natutil and listutil lemmas | 2018-10-10 | |
| | |||
* | Add map_update_nth_ext | 2018-10-09 | |
| | |||
* | Add some util lemmas | 2018-08-13 | |
| | |||
* | Add ListUtil.map_nth_default_seq | 2018-08-10 | |
| | |||
* | Add ListUtil.{combine_repeat,combine_rev_rev_samelength} | 2018-08-09 | |
| | |||
* | Add nth_error_combine | 2018-08-01 | |
| | |||
* | Add more proper instances | 2018-07-26 | |
| | |||
* | Add ListUtil.{take,drop}_while | 2018-07-24 | |
| | |||
* | Add minor lemmas to util | 2018-07-17 | |
| | |||
* | Add ZUtil, list lemmas | 2018-07-02 | |
| | |||
* | Fix a notation issue in previous commit | 2018-07-02 | |
| | |||
* | Add more ListUtil proofs | 2018-07-02 | |
| | |||
* | Add some list lemmas | 2018-07-02 | |
| | |||
* | Add useful list lemmas | 2018-06-29 | |
| | |||
* | Add list_beq | 2018-06-22 | |
| | |||
* | Add seq_add, seq_len_0 | 2018-06-19 | |
| | |||
* | Move function argument out of fixpoint of List.map2 | 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 | 2018-04-11 | |
| | |||
* | pass-through after Andres's review in #334 | 2018-04-03 | |
| | |||
* | move some lemmas to ZUtil/ListUtil | 2018-04-03 | |
| | |||
* | move some lemmas/hints to ListUtil | 2018-04-03 | |
| | |||
* | Add list_case, a definition for match on list | 2018-03-27 | |
| | |||
* | add two proofs about lists | 2018-02-23 | |
| | |||
* | Strip the pointed instance names off of the default value in list expansion | 2018-02-18 | |
| | | | | This is required for reification to work, it seems | ||
* | Add expand_lists tactic | 2018-02-18 | |
| | |||
* | Add expand_list_correct to ListUtil | 2018-02-12 | |
| | |||
* | Generalize Forall2_forall_iff | 2017-11-09 | |
| | |||
* | src/Demo.v: a 200-line introduction to BaseSystem ideas | 2017-06-21 | |
| | |||
* | Don't rely on autogenerated names | 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/ | 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 | 2017-04-06 | |
| | |||
* | Add [Proof using] to most proofs | 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] | 2017-03-24 | |
| | |||
* | Add {firstn,skipn}_seq | 2017-03-19 | |
| | |||
* | generalize In_firstn_skipn_split | 2017-03-19 | |
| | |||
* | Add In_firstn_skipn_split | 2017-03-19 | |
| | |||
* | Add firstn_firstn_min | 2017-03-19 | |
| | |||
* | Fix a name clash | 2017-03-14 | |
| | |||
* | Add firstn_skipn | 2017-03-14 | |
| | |||
* | Add skipn_skipn | 2017-03-14 | |
| | |||
* | added Positional wrappers for Associational operations, added correctness ↵ | 2017-02-27 | |
| | | | | proof of | ||
* | prove admits in Util.Tuple | 2016-11-11 | |
| | |||
* | Add fold_right_andb_true_iff_fold_right_and_True | 2016-10-19 | |
| | |||
* | Add Tuple.map2 | 2016-10-19 | |
| | |||
* | Work around bug #5112 ([Arguments id /] broken) | 2016-09-30 | |
| | |||
* | Move side lemmas to appropriate files | 2016-09-17 | |
| |