diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-25 21:06:07 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-25 21:06:07 -0400 |
| commit | 39a6c95de8a900c859726d875cc40ea96298d31b (patch) | |
| tree | 750571dc101f477c34340716db87a3697cca41eb /src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | |
| parent | ea9397e3da37f35d088488be141cb18cc38ea11b (diff) | |
Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change through the pipeline. Also began the process of redoing canonicalization proofs, attempting to put the messy case analysis in theorem statements rather than separate lemmas.
Diffstat (limited to 'src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v')
0 files changed, 0 insertions, 0 deletions