Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | partition -> Partition.partition to prevent confusion with List.partition | jadep | 2019-04-03 |
| | |||
* | fix imports and qualifiers so everything builds | jadep | 2019-04-03 |
| | |||
* | split up Arithmetic (imports etc. not yet fixed, does not build) | jadep | 2019-04-03 |
| | |||
* | Add constr_fail and constr_fail_with | Jason Gross | 2019-03-31 |
| | | | | | | | | | | | | | Rather than taking the convention that failures during constr construction emit a type error from `I : I` with the actual error message `idtac`d above them (because Coq has no way to emit multiple things on stderr), we instead factor everything through a new `constr_fail` or `constr_fail_with msg_tac`, which emit more helpful messages instructing the user to look in `*coq*` or to use `Fail`/`try` to see the more informative error message. When we can make our own version that does both `idtac` and `fail` (c.f. https://github.com/coq/coq/issues/3913), then we can do something a bit more sane, hopefully. | ||
* | start adapting Montgomery to new glue code | jadep | 2019-02-21 |
| | |||
* | Use Preconditions: Postconditions:, rather than /\ and -> | Jason Gross | 2019-02-02 |
| | |||
* | More minor improvements in docstrings | Jason Gross | 2019-02-02 |
| | |||
* | Rename docstring generator based on Andres' suggestion | Jason Gross | 2019-02-02 |
| | |||
* | Update with davidben's and Andres' suggestions | Jason Gross | 2019-02-02 |
| | |||
* | Drop `map λ` bits in docstrings | Jason Gross | 2019-02-02 |
| | | | | | | | | | They are redundant with the bounds pre- and post-conditions in WBW montgomery. Also drop the fiat_p... prefix from the `from_montgomery` bits in most of the docstrings, under the assumption that shorter strings with less repetition are more readable. | ||
* | Address code review comments to improve docstrings | Jason Gross | 2019-02-02 |
| | |||
* | Add autogenerated docstrings to synthesized code | Jason Gross | 2019-02-02 |
| | | | | | | | | | We now stringify the correctness conditions to generate docstrings for the synthesized code. Closes #512 Time commitment: about 6 hours | ||
* | Also display the carry chain in a comment | Jason Gross | 2019-01-26 |
| | |||
* | Split up PushButtonSynthesis.v | Jason Gross | 2019-01-18 |
Closes #497 |