diff --git a/theories/list_numbers.v b/theories/list_numbers.v index 556ea185266739edeeac33a9d33935c665855730..aaa8564acb4ff7cafa1955aee1124435b97b6c76 100644 --- a/theories/list_numbers.v +++ b/theories/list_numbers.v @@ -30,8 +30,8 @@ Notation max_list := (max_list_with id). (** [Z_to_little_endian m n z] converts [z] into a list of [m] [n]-bit integers in the little endian format. A negative [z] is encoded using two's-complement. If [z] uses more than [m * n] bits, these additional -bits are discarded (see [Z_to_little_endian_to_Z]). [n] should be non-negative. -*) +bits are discarded (see [Z_to_little_endian_to_Z]). [m] and [n] should be +non-negative. *) Definition Z_to_little_endian (m n : Z) : Z → list Z := Z.iter m (λ rec z, Z.land z (Z.ones n) :: rec (z ≫ n)%Z) (λ _, []). Global Arguments Z_to_little_endian : simpl never.