| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Fix 8.4 build issues |  Jason Gross | 2016-12-15 |
| * | Fix 8.4 issues | Jason Gross | 2016-12-15 |
| * | Work around bug in 8.4 implicits | Jason Gross | 2016-12-14 |
| * | Work around bug in 8.4 apply | Jason Gross | 2016-12-14 |
| * | Admit Common9_4Op.v | Jason Gross | 2016-12-08 |
| * | Don't use UIP in inversion_wff | Jason Gross | 2016-12-03 |
| * | Add inversion_wff | Jason Gross | 2016-12-03 |
| * | Add WfInversion | Jason Gross | 2016-12-03 |
| * | More powerful inversion_option | Jason Gross | 2016-12-03 |
| * | Move things to ExprInversion | Jason Gross | 2016-12-03 |
| * | Add invert_Var | Jason Gross | 2016-12-03 |
| * | Arguments for invert_Op | Jason Gross | 2016-12-03 |
| * | Fewer autogenerated names | Jason Gross | 2016-12-03 |
| * | Add invert_Op | Jason Gross | 2016-12-03 |
| * | Change some default names | Jason Gross | 2016-12-03 |
| * | copy_bounds.sh | Jason Gross | 2016-12-02 |
| * | Fix looping in Coq 8.4 in ExtendedAddCoordinates.v | Jason Gross | 2016-12-02 |
| * | Initial (not fully working) version of MapWithInterpInfo | Jason Gross | 2016-12-02 |
| * | Add SmartFlatTypeMapUnInterp | Jason Gross | 2016-12-02 |
| * | Add invert_LetIn | Jason Gross | 2016-12-02 |
| * | Arguments for invert_Pair | Jason Gross | 2016-12-02 |
| * | Add invert_Pair | Jason Gross | 2016-12-02 |
| * | Add SmartFlatTypeMapInterp | Jason Gross | 2016-12-02 |
| * | SmartFlatTypeMap arguments | Jason Gross | 2016-12-02 |
| * | Add SmartFlatTypeMap | Jason Gross | 2016-12-02 |
| * | Minor change to inm_op_correct_and_bounded_prefix | Jason Gross | 2016-11-25 |
| * | Fix a typo | Jason Gross | 2016-11-25 |
| * | Add inm_op_correct_and_bounded_iff_prefix | Jason Gross | 2016-11-25 |
| * | Add inm_op_correct_and_bounded | Jason Gross | 2016-11-25 |
| * | Also git add in copy_bounds | Jason Gross | 2016-11-25 |
| * | uncurry_n_op_fe25519 | Jason Gross | 2016-11-25 |
| * | Various application lemmas | Jason Gross | 2016-11-23 |
| * | More GF25519ReflectiveCommon generalization | Jason Gross | 2016-11-22 |
| * | Add tuple lemmas | Jason Gross | 2016-11-22 |
| * | Add lemmas about application | Jason Gross | 2016-11-22 |
| * | Add impl_under_tower | Jason Gross | 2016-11-22 |
| * | Add hlistP | Jason Gross | 2016-11-22 |
| * | Add rhlist | Jason Gross | 2016-11-22 |
| * | Add interp_all_binders_for' | Jason Gross | 2016-11-22 |
| * | Add tower_nd | Jason Gross | 2016-11-22 |
| * | Fix for 8.6 | Jason Gross | 2016-11-22 |
| * | Copy bounds, fix a typo | Jason Gross | 2016-11-22 |
| * | Start work on a faster version of GF*Reflective/Common* | Jason Gross | 2016-11-21 |
| * | Fix for Coq 8.4 | Jason Gross | 2016-11-21 |
| * | Fix missing import for List.repeat in 8.4 | Jason Gross | 2016-11-21 |
| * | Better extraction | Jason Gross | 2016-11-17 |
| * | Copy bounds | Jason Gross | 2016-11-17 |
| * | Finish proofs about eliminating useless carries | Jason Gross | 2016-11-17 |
| * | Add add_coordinates_respectful_hetero | Jason Gross | 2016-11-17 |
| * | Remove an admit | Jason Gross | 2016-11-17 |
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |