Update with davidben's and Andres' suggestions

1 files changed, 1 insertions, 1 deletions

diff --git a/p256_32.c b/p256_32.c
index 1bfabfaa7..b4742b2dd 100644
--- a/p256_32.c
+++ b/p256_32.c
@@ -57,7 +57,7 @@ static void fiat_p256_subborrowx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat
 }
 
 /*
- * The function fiat_p256_mulx_u32 is an extended multiplication.
+ * The function fiat_p256_mulx_u32 is a multiplication, returning the full double-width result.
  * out1 = (arg1 * arg2) mod 2^32
  * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋
  * Input Bounds: