diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-30 23:32:26 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-02-02 18:22:15 -0500 |
| commit | ad2af1d46963f9496d56a6185100fb34199854e7 (patch) | |
| tree | 0b50ac6e5418ed0ba7060c4c33d07736c99169ee /src/PushButtonSynthesis/WordByWordMontgomery.v | |
| parent | 6fbafbb3a90a5491103e0044042bfc726b9eab7b (diff) | |
Drop `map λ` bits in docstrings
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.
Diffstat (limited to 'src/PushButtonSynthesis/WordByWordMontgomery.v')
| -rw-r--r-- | src/PushButtonSynthesis/WordByWordMontgomery.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v index 46ffa083f..d95f35bf4 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomery.v +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -235,10 +235,11 @@ Section __. (CorrectnessStringification.dyn_context.cons r' ("((2^" ++ decimal_string_of_Z machine_wordsize ++ ")⁻¹ mod m)")%string (CorrectnessStringification.dyn_context.cons - from_montgomery_res (prefix ++ "from_montgomery")%string + from_montgomery_res "from_montgomery"%string (CorrectnessStringification.dyn_context.cons (@eval 8 n_bytes) "bytes_eval"%string - CorrectnessStringification.dyn_context.nil)))). + CorrectnessStringification.dyn_context.nil)))) + (only parsing). Local Notation stringify_correctness prefix pre_extra correctness := (stringify_correctness_with_ctx (initial_ctx prefix) |