diff options
Diffstat (limited to 'src/PushButtonSynthesis/SaturatedSolinas.v')
| -rw-r--r-- | src/PushButtonSynthesis/SaturatedSolinas.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v index 6de66a50f..47431eb09 100644 --- a/src/PushButtonSynthesis/SaturatedSolinas.v +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -138,8 +138,8 @@ 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 "'docstring_with_summary_from_lemma!' pre_extra correctness" + := (docstring_with_summary_from_lemma_with_ctx! initial_ctx evalf pre_extra @@ -161,7 +161,7 @@ Section __. := Eval cbv beta in FromPipelineToString prefix "mul" mul - (stringify_correctness! + (docstring_with_summary_from_lemma! (fun fname : string => ["The function " ++ fname ++ " multiplies two field elements."]%string) (mul_correct weightf n m boundsn)). |