diff --git a/theories/bitvector.v b/theories/bitvector.v
index a8255a4a08ea00185a7800a3722500bab7da682c..798d2111a4855594c3c9b48d976629f56c2391e2 100644
--- a/theories/bitvector.v
+++ b/theories/bitvector.v
@@ -517,7 +517,9 @@ Program Definition bv_sign_extend {n} (z : N) (b : bv n) : bv (n + z) := (* SMT:
 
 (* s is start index and l is length. Note that this is different from
 extract in SMTLIB which uses [extract (inclusive upper bound)
-(inclusive lower bound)] *)
+(inclusive lower bound)]. The version here is phrased in a way that
+makes it impossible to use an upper bound that is lower than the lower
+bound. *)
 Program Definition bv_extract {n} (s l : N) (b : bv n) : bv l :=
   BV l (Z.land (bv_unsigned b ≫ Z.of_N s) (Z.ones (Z.of_N l))) _.
 Next Obligation.