diff options
Diffstat (limited to 'src/PushButtonSynthesis/SaturatedSolinas.v')
| -rw-r--r-- | src/PushButtonSynthesis/SaturatedSolinas.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v index 2549d190a..6de66a50f 100644 --- a/src/PushButtonSynthesis/SaturatedSolinas.v +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -138,13 +138,13 @@ Section __. Local Notation weightf := (weight machine_wordsize 1). Local Notation evalf := (eval weightf n). Local Notation initial_ctx := (CorrectnessStringification.dyn_context.nil). - Local Notation stringify_correctness pre_extra correctness - := (stringify_correctness_with_ctx + Local Notation "'stringify_correctness!' pre_extra correctness" + := (stringify_correctness_with_ctx! initial_ctx evalf pre_extra correctness) - (only parsing). + (only parsing, at level 10, pre_extra at next level, correctness at next level). Definition mul := Pipeline.BoundsPipeline @@ -161,7 +161,7 @@ Section __. := Eval cbv beta in FromPipelineToString prefix "mul" mul - (stringify_correctness + (stringify_correctness! (fun fname : string => ["The function " ++ fname ++ " multiplies two field elements."]%string) (mul_correct weightf n m boundsn)). |