| Commit message (Expand) | Author | Age |
|---|
| * | Add Tuple.map_Proper |  Jason Gross | 2017-04-03 |
| * | More fine-grained tactic imports | Jason Gross | 2017-04-03 |
| * | Split off liftn_sig, add lift{3,4}_sig | Jason Gross | 2017-04-03 |
| * | Fix parsing issue | Jason Gross | 2017-04-03 |
| * | Add proj2_sig_map | Jason Gross | 2017-04-03 |
| * | Don't require keeping track of which goals have evars; check that in tactics | Jason Gross | 2017-04-03 |
| * | Add UnifyAbstractReflexivity tactics | Jason Gross | 2017-04-03 |
| * | Fix a typo | Jason Gross | 2017-04-02 |
| * | Add projT2_map | Jason Gross | 2017-04-02 |
| * | Add Tactics.EvarExists | Jason Gross | 2017-04-02 |
| * | Add Util.SigmaAssoc | Jason Gross | 2017-04-02 |
| * | Add ap_transport to Equality.v | Jason Gross | 2017-04-02 |
| * | Coalesce Tuple.pointwise2 and Tuple.fieldwise | Jason Gross | 2017-04-02 |
| * | Fix definition of BoundedWord | Jason Gross | 2017-04-01 |
| * | Split off BoundedWord.v from IntegrationTest.v | Jason Gross | 2017-04-01 |
| * | Split out Tactics.SubstLet | Jason Gross | 2017-04-01 |
| * | Add Tuple.eta | Jason Gross | 2017-04-01 |
| * | Add Z.log2_up_le_pow2_full | Jason Gross | 2017-03-31 |
| * | Add is_tighter_than_bool to zrange | Jason Gross | 2017-03-31 |
| * | More compatibility for etransitivity | Jason Gross | 2017-03-31 |
| * | Add [change_with_curried] to Curry.v | Jason Gross | 2017-03-31 |
| * | Add [etransitivity y], [etransitivity_rev] tactics | Jason Gross | 2017-03-31 |
| * | Add wordToZ{_gen,}_range | Jason Gross | 2017-03-30 |
| * | added tuple [repeat] |  jadep | 2017-03-30 |
| * | Use r[_ ~> _] for range rather than b[_ ~> _] | Jason Gross | 2017-03-30 |
| * | Rename Bounds to ZRange, use Prop, not bool | Jason Gross | 2017-03-30 |
| * | Get rid of list-based Tuple.map | Jason Gross | 2017-03-30 |
| * | Add a file dedicated to the definition of Z bounds | Jason Gross | 2017-03-30 |
| * | Add Tuple.pointwise2, Tuple.map_fix | Jason Gross | 2017-03-30 |
| * | remove commented-out lemma and add CPS version of mapi_with | jadep | 2017-03-29 |
| * | change map_with to mapi_with, a version that handles the index explicitly | jadep | 2017-03-29 |
| * | Add Z.one_succ Z.two_succ to zsimplify_const db | Jason Gross | 2017-03-28 |
| * | Don't reserve '(max_bitwidth' | Jason Gross | 2017-03-28 |
| * | Add a notation for printing | Jason Gross | 2017-03-28 |
| * | Add lemmas needed for saturated arithmetic [compact] | jadep | 2017-03-24 |
| * | Split off extra power of ltb_to_lt, split_andb | Jason Gross | 2017-03-21 |
| * | Remove a line I forgot to remove in the previous commit | Jason Gross | 2017-03-21 |
| * | Split off the extra power of rewrite_mod_small into rewrite_mod_mod_small | Jason Gross | 2017-03-21 |
| * | Make Z.rewrite_mod_small a bit more powerful | Jason Gross | 2017-03-21 |
| * | Make Bool.split_andb a bit more powerful | Jason Gross | 2017-03-21 |
| * | Make Z.ltb_to_lt a bit stronger | Jason Gross | 2017-03-21 |
| * | 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 |
| * | Add dec_eq_positive | Jason Gross | 2017-03-17 |
| * | Fix a name clash | Jason Gross | 2017-03-14 |
| * | Add firstn_skipn | Jason Gross | 2017-03-14 |
| * | Add split_prod | Jason Gross | 2017-03-14 |
| * | Add skipn_skipn | Jason Gross | 2017-03-14 |
Jason Gross
jadep