]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataTypes.ml
added support for hits table
[helm.git] / helm / ocaml / metadata / metadataTypes.ml
index 51f79c8288c9e9c6cecddb310f434df4618fd264..5284d96b5dd48377585ce62d8133cd0459dd824e 100644 (file)
@@ -69,6 +69,7 @@ let rel_tbl_original = "refRel"
 let obj_tbl_original = "refObj"
 let name_tbl_original = "objectName"
 let count_tbl_original = "count"
+let hits_tbl_original = "hits"
 
   (** the names currently used *)
 let sort_tbl_real = ref sort_tbl_original
@@ -98,6 +99,7 @@ let library_rel_tbl = rel_tbl_original
 let library_obj_tbl = obj_tbl_original
 let library_name_tbl = name_tbl_original
 let library_count_tbl = count_tbl_original
+let library_hits_tbl = hits_tbl_original
 
 let are_tables_ownerized () =
   sort_tbl () <> library_sort_tbl