X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.mli;h=725192ebc943bbdbc88c9a8307bf912f3d790ff9;hp=579dd8a81cb182da3a79c4b83dba3d899fc20fa0;hb=e56b9fbeaed04c1f2fb7019de34f7d8e87d6db73;hpb=22d98520210487a6ad8cd70c3fa711c382ffa6ca

diff --git a/src/run.mli b/src/run.mli
index 579dd8a..725192e 100644
--- a/src/run.mli
+++ b/src/run.mli
@@ -14,10 +14,10 @@
 (***********************************************************************)
 type stats = { run : int;
                tree_size : int;
-               cache2_access : int;
-               cache2_hit : int;
-               cache5_access : int;
-               cache5_hit : int;
+               fetch_trans_cache_access : int;
+               fetch_trans_cache_hit : int;
+               eval_trans_cache_access : int;
+               eval_trans_cache_hit : int;
              }
 module Make (T : Tree.S) :
   sig