Commit message (Expand) | Author | Age | |
---|---|---|---|
* | More fine-grained tactic imports | 2017-04-03 | |
* | Add invert_Some; add nat_N_Z to push_Zof_N | 2017-02-23 | |
* | Work around bug in 8.4 apply | 2016-12-14 | |
* | More powerful inversion_option | 2016-12-03 | |
* | Fix for Coq 8.5, 8.5pl1 | 2016-10-18 | |
* | generalize equiv relations in Util.Option and EdDSARepChange | 2016-10-12 | |
* | Fix for Coq 8.5 | 2016-09-16 | |
* | Derive EdDSA.verify from equational specification | 2016-09-16 | |
* | Make [inversion_option] work on Prop options | 2016-09-03 | |
* | Rename congrunce_option to inversion_option, add [inversion_prod] | 2016-08-31 | |
* | Add congruence_option tactic | 2016-08-31 | |
* | added proofs about addition chain exponentiation for later use in ModularBase... | 2016-07-10 | |
* | EdDSA: prove things about spec | 2016-06-25 |