| Commit message (Collapse) | Author | Age |
|
|
|
| |
See PR #220 https://github.com/coq/coq/pull/220
|
| |
|
|
|
|
|
|
| |
This fixes all of the private-names warnings emitted by
compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus
the ones in coqprime, which I didn't touch).
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
This closes #146 and makes `make quick` faster.
The changes were generated by adding [Global Set Suggest Proof Using.]
to GlobalSettings.v, and then following [the instructions for a script I
wrote](https://github.com/JasonGross/coq-tools#proof-using-helper).
|
| |
|
|
|
|
| |
This way they won't become ambiguous if we add new files
|
| |
|
|
|
|
| |
correctness is in terms of N rather than nat; this allows us to compute the correctness proof for large exponents.
|
|
|
|
|
|
|
|
|
|
|
|
| |
ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.
Backwards-incompatible changes:
F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1
|
|
ModularBaseSystem [pow], which we need for sqrt and inversion.
|