diff options
| -rw-r--r-- | otherlibs/num/nat.mlp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/otherlibs/num/nat.mlp b/otherlibs/num/nat.mlp index 90877d521..699b7ed33 100644 --- a/otherlibs/num/nat.mlp +++ b/otherlibs/num/nat.mlp @@ -259,7 +259,7 @@ let raw_string_of_digit nat off = (* XL: suppression de string_of_digit et de sys_string_of_digit. La copie est de toute facon faite dans string_of_nat, qui est le - seul point d'entree public dans ce code. *) + seul point d entree public dans ce code. *) (****** let sys_string_of_digit nat off = |