aboutsummaryrefslogtreecommitdiff
path: root/kernel/uint31.mli
diff options
context:
space:
mode:
authorEnrico Tassi2015-02-23 17:14:05 +0100
committerEnrico Tassi2015-02-23 17:14:05 +0100
commite87ca456fb4cbe54f09e13f1e20d504d2699ac2b (patch)
tree41b358ee2deb7c614e39f7db27368f9626c19778 /kernel/uint31.mli
parent28781f3fd6ae6e7f281f906721e8a028679ca089 (diff)
parentdf2f50db3703b4f7f88f00ac382c7f3f1efaceb3 (diff)
Merge branch 'v8.5' into trunk
Diffstat (limited to 'kernel/uint31.mli')
-rw-r--r--kernel/uint31.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/uint31.mli b/kernel/uint31.mli
index e8b980809d..d1f933cc4e 100644
--- a/kernel/uint31.mli
+++ b/kernel/uint31.mli
@@ -5,7 +5,7 @@ val to_int : t -> int
val of_int : int -> t
val of_uint : int -> t
- (* convertion to a string *)
+ (* conversion to a string *)
val to_string : t -> string
val of_string : string -> t