aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/int.ml
diff options
context:
space:
mode:
authorGravatar Xavier Clerc <xavier.clerc@inria.fr>2014-09-25 11:02:00 +0200
committerGravatar Xavier Clerc <xavier.clerc@inria.fr>2014-09-25 11:02:00 +0200
commit4e1135fb315eab7bede3861e83e0ced74cf60ed3 (patch)
tree4a67d742c88df6bd2cb6b1ba203099801a36bd81 /lib/int.ml
parent31205e035316a7795ee3a1e0045148194cdcfcae (diff)
Remove some 'deprecated' warnings.
Diffstat (limited to 'lib/int.ml')
-rw-r--r--lib/int.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/int.ml b/lib/int.ml
index 1403dc510..c8786c8a2 100644
--- a/lib/int.ml
+++ b/lib/int.ml
@@ -64,7 +64,7 @@ struct
| Root of 'a option array
| DSet of int * 'a option * 'a t
- let empty n = ref (Root (Array.create n None))
+ let empty n = ref (Root (Array.make n None))
let rec rerootk t k = match !t with
| Root _ -> k ()