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