| Commit message (Expand) | Author | Age |
|---|
| * | Add Zpow_sub_1_nat_pow |  Jason Gross | 2017-11-03 |
| * | Add value_modulo_in_range | Jason Gross | 2017-11-03 |
| * | Better version of ZBounded.modulo, with a proof | Jason Gross | 2017-11-03 |
| * | Add ZBounded.modulo | Jason Gross | 2017-11-03 |
| * | Add type of bounded Z | Jason Gross | 2017-11-02 |
| * | Add cps versions of id_with_alt | Jason Gross | 2017-11-01 |
| * | add ZToSignedWord, signedWordToZ | Jason Gross | 2017-10-31 |
| * | Factor out fold_right_cps2_specialized_step, add mapi_with'_cps2 | Jason Gross | 2017-10-22 |
| * | Add curry{3,4} | Jason Gross | 2017-10-20 |
| * | Switch arithmetic to cps for Z * Z under the hood | Jason Gross | 2017-10-19 |
| * | Add mul_split_cps' | Jason Gross | 2017-10-19 |
| * | Update ZUtil cps definitions | Jason Gross | 2017-10-19 |
| * | Add ZUtil.CPS | Jason Gross | 2017-10-19 |
| * | Add 8.7-only CacheTerm | Jason Gross | 2017-10-18 |
| * | Add a Require Import FunInd (Function isn't loaded by default anymore) |  Pierre Letouzey | 2017-10-18 |
| * | Allow instantiating type arguments without reducing matches | Jason Gross | 2017-10-18 |
| * | Allow instantiating type arguments without reducing matches | Jason Gross | 2017-10-17 |
| * | Allow instantiating type arguments without reducing matches | Jason Gross | 2017-10-17 |
| * | Allow instantiation of cps type arguments by unfolding | Jason Gross | 2017-10-17 |
| * | Add CacheTerm | Jason Gross | 2017-10-17 |
| * | Allow unfolding of mapi_with_cps to specialize the function to the type argum... | Jason Gross | 2017-10-17 |
| * | Work around bug #5341 | Jason Gross | 2017-10-17 |
| * | Add strip_subst_local | Jason Gross | 2017-10-15 |
| * | Add pow_ceil_mul_nat_divide_upperbound | Jason Gross | 2017-10-13 |
| * | Add reflective compose, notation for Z.Syntax.{Expr,Interp} | Jason Gross | 2017-10-12 |
| * | Add update_by_tac_if_not_exists | Jason Gross | 2017-10-10 |
| * | TagList: make get error, and fix bugs | Jason Gross | 2017-10-10 |
| * | Add TagList | Jason Gross | 2017-10-10 |
| * | Add notations | Jason Gross | 2017-10-10 |
| * | Add pow_ceil_mul_nat_nonneg | Jason Gross | 2017-10-05 |
| * | Add PoseTermWithName | Jason Gross | 2017-10-05 |
| * | Add some ZUtil lemmas | Jason Gross | 2017-10-03 |
| * | Add decidable equality with nil | Jason Gross | 2017-08-13 |
| * | Make some tactics a bit more powerful | Jason Gross | 2017-07-08 |
| * | More fine-grained tactics imports | Jason Gross | 2017-07-08 |
| * | More fine-grained imports | Jason Gross | 2017-07-08 |
| * | Add UnfoldArg | Jason Gross | 2017-07-08 |
| * | prove an admit in ArithmeticSynthesisTest |  Andres Erbsen | 2017-07-06 |
| * | Add wrappers for subborrow and add_with_get_carry so they work when it is not... |  jadep | 2017-06-29 |
| * | remove unused admit (has been moved to Tuple.v) | jadep | 2017-06-26 |
| * | Prove map2_append | Jason Gross | 2017-06-25 |
| * | write and prove Tuple.map2_cps | jadep | 2017-06-25 |
| * | Fix a typo in push_Zmod that was causing looping | Jason Gross | 2017-06-22 |
| * | Fix some minor naming bugs in sig_assoc tactics | Jason Gross | 2017-06-22 |
| * | src/Demo.v: a 200-line introduction to BaseSystem ideas | Andres Erbsen | 2017-06-21 |
| * | Prove In_to_list_left_tl, In_left_hd, to_list_left_append | Jason Gross | 2017-06-21 |
| * | Add is_bounded_by_None_repeat_In_iff_lt | Jason Gross | 2017-06-20 |
| * | Add fold_left_orb_true, fold_left_orb_pull | Jason Gross | 2017-06-20 |
| * | Add is_bounded_by_None_repeat_In_iff | Jason Gross | 2017-06-20 |
| * | [Require NatUtil] should not change [tauto] | Jason Gross | 2017-06-19 |
Jason Gross
Pierre Letouzey
Andres Erbsen
jadep