diff options
Diffstat (limited to 'theories/Strings/Ascii.v')
| -rw-r--r-- | theories/Strings/Ascii.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 87d8e1350..1f90c06cf 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -59,7 +59,7 @@ Defined. looking at the last n bits, ie z mod 2^n *) Fixpoint ascii_of_pos_aux (res acc : ascii) (z : positive) - (n : nat) {struct n} : ascii := + (n : nat) : ascii := match n with | O => res | S n1 => |