diff options
Diffstat (limited to 'src/PushButtonSynthesis/MontgomeryReduction.v')
| -rw-r--r-- | src/PushButtonSynthesis/MontgomeryReduction.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/PushButtonSynthesis/MontgomeryReduction.v b/src/PushButtonSynthesis/MontgomeryReduction.v index 2b7841ac0..a452a047c 100644 --- a/src/PushButtonSynthesis/MontgomeryReduction.v +++ b/src/PushButtonSynthesis/MontgomeryReduction.v @@ -82,7 +82,10 @@ Section rmontred. Definition smontred (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "montred" montred. + := Eval cbv beta in + FromPipelineToString + prefix "montred" montred + (fun _ _ _ => @nil string). (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like << |