Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Update .travis.yml | 2016-12-05 | |
| | |||
* | Only test 8.6beta1 on travis | 2016-12-05 | |
| | |||
* | Don't use UIP in inversion_wff | 2016-12-03 | |
| | |||
* | Add inversion_wff | 2016-12-03 | |
| | |||
* | Add WfInversion | 2016-12-03 | |
| | |||
* | More powerful inversion_option | 2016-12-03 | |
| | |||
* | Move things to ExprInversion | 2016-12-03 | |
| | |||
* | Add invert_Var | 2016-12-03 | |
| | |||
* | Arguments for invert_Op | 2016-12-03 | |
| | |||
* | Fewer autogenerated names | 2016-12-03 | |
| | |||
* | Add invert_Op | 2016-12-03 | |
| | |||
* | Change some default names | 2016-12-03 | |
| | |||
* | copy_bounds.sh | 2016-12-02 | |
| | |||
* | Fix looping in Coq 8.4 in ExtendedAddCoordinates.v | 2016-12-02 | |
| | |||
* | Initial (not fully working) version of MapWithInterpInfo | 2016-12-02 | |
| | |||
* | Add SmartFlatTypeMapUnInterp | 2016-12-02 | |
| | |||
* | Add invert_LetIn | 2016-12-02 | |
| | |||
* | Arguments for invert_Pair | 2016-12-02 | |
| | |||
* | Add invert_Pair | 2016-12-02 | |
| | |||
* | Add SmartFlatTypeMapInterp | 2016-12-02 | |
| | |||
* | SmartFlatTypeMap arguments | 2016-12-02 | |
| | |||
* | Add SmartFlatTypeMap | 2016-12-02 | |
| | |||
* | Minor change to inm_op_correct_and_bounded_prefix | 2016-11-25 | |
| | |||
* | Fix a typo | 2016-11-25 | |
| | |||
* | Add inm_op_correct_and_bounded_iff_prefix | 2016-11-25 | |
| | |||
* | Add inm_op_correct_and_bounded | 2016-11-25 | |
| | |||
* | Also git add in copy_bounds | 2016-11-25 | |
| | |||
* | uncurry_n_op_fe25519 | 2016-11-25 | |
| | |||
* | Various application lemmas | 2016-11-23 | |
| | |||
* | More GF25519ReflectiveCommon generalization | 2016-11-22 | |
| | |||
* | Add tuple lemmas | 2016-11-22 | |
| | |||
* | Add lemmas about application | 2016-11-22 | |
| | |||
* | Add impl_under_tower | 2016-11-22 | |
| | |||
* | Add hlistP | 2016-11-22 | |
| | |||
* | Add rhlist | 2016-11-22 | |
| | |||
* | Add interp_all_binders_for' | 2016-11-22 | |
| | |||
* | Add tower_nd | 2016-11-22 | |
| | |||
* | Fix for 8.6 | 2016-11-22 | |
| | |||
* | Copy bounds, fix a typo | 2016-11-22 | |
| | |||
* | Start work on a faster version of GF*Reflective/Common* | 2016-11-21 | |
| | |||
* | Fix for Coq 8.4 | 2016-11-21 | |
| | |||
* | Fix missing import for List.repeat in 8.4 | 2016-11-21 | |
| | |||
* | Don't let travis kill us in 10 minutes of silence | 2016-11-18 | |
| | |||
* | Better extraction | 2016-11-17 | |
| | |||
* | Copy bounds | 2016-11-17 | |
| | | | | | | | ```bash $ pushd src/SpecificGen; pushd $ pushd && for i in *.json; do ./copy_bounds.sh $i; done && pushd ``` | ||
* | Finish proofs about eliminating useless carries | 2016-11-17 | |
| | |||
* | Add add_coordinates_respectful_hetero | 2016-11-17 | |
| | |||
* | Remove an admit | 2016-11-17 | |
| | |||
* | Add fieldwise_map | 2016-11-17 | |
| | |||
* | Add another admitted lemma | 2016-11-17 | |
| |