diff options
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) |