aboutsummaryrefslogtreecommitdiff
path: root/src/PushButtonSynthesis/SaturatedSolinas.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/PushButtonSynthesis/SaturatedSolinas.v')
-rw-r--r--src/PushButtonSynthesis/SaturatedSolinas.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v
index 7ff799c80..2549d190a 100644
--- a/src/PushButtonSynthesis/SaturatedSolinas.v
+++ b/src/PushButtonSynthesis/SaturatedSolinas.v
@@ -162,7 +162,7 @@ Section __.
FromPipelineToString
prefix "mul" mul
(stringify_correctness
- (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+ (fun fname : string => ["The function " ++ fname ++ " multiplies two field elements."]%string)
(mul_correct weightf n m boundsn)).
Local Ltac solve_extra_bounds_side_conditions :=