From 32b7a0cc9c8302febd7639d22c80554fa4ec8d88 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Wed, 19 Dec 2012 00:13:21 +0000
Subject: Array.create is deprecated

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16104 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/cc/ccalgo.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index f029c053a3..21077ecc88 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -241,7 +241,7 @@ let empty depth gls:state =
   {uf=
      {max_size=init_size;
       size=0;
-      map=Array.create init_size dummy_node;
+      map=Array.make init_size dummy_node;
       epsilons=[];
       axioms=Constrhash.create init_size;
       syms=Termhash.create init_size};
@@ -335,7 +335,7 @@ let next uf=
   let nsize= succ size in
     if nsize=uf.max_size then
       let newmax=uf.max_size * 3 / 2 + 1 in
-      let newmap=Array.create newmax dummy_node in
+      let newmap=Array.make newmax dummy_node in
 	begin
 	  uf.max_size<-newmax;
 	  Array.blit uf.map 0 newmap 0 size;
-- 
cgit v1.2.3