diff options
Diffstat (limited to 'src/PushButtonSynthesis/SaturatedSolinas.v')
| -rw-r--r-- | src/PushButtonSynthesis/SaturatedSolinas.v | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v index 47431eb09..0e7aaf6b2 100644 --- a/src/PushButtonSynthesis/SaturatedSolinas.v +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -137,14 +137,18 @@ Section __. Local Notation weightf := (weight machine_wordsize 1). Local Notation evalf := (eval weightf n). - Local Notation initial_ctx := (CorrectnessStringification.dyn_context.nil). - Local Notation "'docstring_with_summary_from_lemma!' pre_extra correctness" + Local Notation notations_for_docstring + := (CorrectnessStringification.dyn_context.cons + weightf "weight" + (CorrectnessStringification.dyn_context.cons + evalf "eval" + CorrectnessStringification.dyn_context.nil))%string. + Local Notation "'docstring_with_summary_from_lemma!' summary correctness" := (docstring_with_summary_from_lemma_with_ctx! - initial_ctx - evalf - pre_extra + notations_for_docstring + summary correctness) - (only parsing, at level 10, pre_extra at next level, correctness at next level). + (only parsing, at level 10, summary at next level, correctness at next level). Definition mul := Pipeline.BoundsPipeline |