Array.create is deprecated

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16104 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 2 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index f029c053a..21077ecc8 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;