Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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). | ||
* | prove compact obeys div/mod rule | jadep | 2017-05-01 |
| | |||
* | added [lastn] for tuples | jadep | 2017-05-01 |
| | |||
* | Fix nth_default for the tip of v8.6 | Jason Gross | 2017-04-28 |
| | | | | | This is bug #5497, https://coq.inria.fr/bugs/show_bug.cgi?id=5497, Coq v8.6 has weaker pattern matching than Coq 8.6 (regression) | ||
* | add nth_default on tuple | jadep | 2017-04-28 |
| | |||
* | 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 Tuple.map_Proper | Jason Gross | 2017-04-03 |
| | |||
* | Coalesce Tuple.pointwise2 and Tuple.fieldwise | Jason Gross | 2017-04-02 |
| | | | | | | We don't need both of them. We keep the definition of pointwise2 because it's needed for reification to work, and we keep the name of fieldwise because it's used in more places. This closes #137. | ||
* | Add Tuple.eta | Jason Gross | 2017-04-01 |
| | |||
* | added tuple [repeat] | jadep | 2017-03-30 |
| | |||
* | Get rid of list-based Tuple.map | Jason Gross | 2017-03-30 |
| | |||
* | Add Tuple.pointwise2, Tuple.map_fix | Jason Gross | 2017-03-30 |
| | | | | These are for definining boundedness and lining up judgmentally with reflective things | ||
* | change map_with to mapi_with, a version that handles the index explicitly | jadep | 2017-03-29 |
| | |||
* | Add lemmas needed for saturated arithmetic [compact] | jadep | 2017-03-24 |
| | |||
* | Add strip_eta_tuple lemmas | Jason Gross | 2017-02-28 |
| | |||
* | Better tuple_eta arguments | Jason Gross | 2017-02-28 |
| | |||
* | Add eta_tuple functions | Jason Gross | 2017-02-28 |
| | | | | | These are for getting nicely reduced forms of, e.g., Tuple.map, without knowing exactly what the tuple is | ||
* | More fine-grained util tactic files | Jason Gross | 2017-01-17 |
| | | | | Also, add [split_and] | ||
* | More universe fixes | Jason Gross | 2017-01-15 |
| | |||
* | Fix an issue with universes | Jason Gross | 2017-01-15 |
| | | | | | | We don't want to force the universe of [option] below other universes; to get template polymorphism to refresh universes, we need to eta-expand [option]. | ||
* | Add tuple lemmas | Jason Gross | 2016-11-22 |
| | |||
* | Add fieldwise_map | Jason Gross | 2016-11-17 |
| | |||
* | use @implicits in rewrite (8.4) | Andres Erbsen | 2016-11-11 |
| | |||
* | prove admits in Util.Tuple | Andres Erbsen | 2016-11-11 |
| | |||
* | Add Tuple and HList lemmas | Jason Gross | 2016-11-10 |
| | |||
* | Fix bug in 8.4 | Jason Gross | 2016-11-09 |
| | |||
* | Add assoc_right | Jason Gross | 2016-11-09 |
| | |||
* | Fix Tuple.map2_S | Jason Gross | 2016-11-09 |
| | |||
* | Add Tuple.map2_S | Jason Gross | 2016-11-08 |
| | |||
* | Add map2_map{,_fst,_snd} | Jason Gross | 2016-11-08 |
| | |||
* | Rename iffT, add some lemmas about tuple and hlist | Jason Gross | 2016-11-08 |
| | | | | Some lemmas admitted | ||
* | Work around bug in 8.4 | Jason Gross | 2016-11-08 |
| | |||
* | Add push_lift_option | Jason Gross | 2016-11-07 |
| | |||
* | Add tuple hd and tl | Jason Gross | 2016-11-07 |
| | |||
* | Add more admitted tuple lemmas | Jason Gross | 2016-11-06 |
| | |||
* | Add more admitted tuple lemmas | Jason Gross | 2016-11-06 |
| | |||
* | Add Tuple.map_map2 (admitted) | Jason Gross | 2016-11-06 |
| | |||
* | Add admitted lemma about tuple map, add hlist lem | Jason Gross | 2016-11-06 |
| | |||
* | Add Tuple lift push | Jason Gross | 2016-11-06 |
| | |||
* | Add functions for [tuple (option _) _] | Jason Gross | 2016-11-06 |
| | |||
* | Move hlist to new file | Jason Gross | 2016-11-01 |
| | |||
* | Fix a typo in the previous commit | Jason Gross | 2016-11-01 |
| | |||
* | Generalize hlist | Jason Gross | 2016-11-01 |
| | |||
* | Add hlist to tuple | Jason Gross | 2016-11-01 |
| | |||
* | Fix implicit status of curry | Jason Gross | 2016-10-27 |
| | |||
* | Add curry and uncurry to tuple | Jason Gross | 2016-10-27 |
| | |||
* | Fix for Coq 8.4 | Jason Gross | 2016-10-24 |
| | |||
* | Add more relations about fieldwise | Jason Gross | 2016-10-24 |
| | |||
* | Add Tuple.map2 | Jason Gross | 2016-10-19 |
| | |||
* | Ed25519: add basepoint and prove most EdDSA preconditions | Andres Erbsen | 2016-10-10 |
| |