X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataDb.ml;h=6cbfeb1ff12e3a47d464d02da468c2d428258538;hb=44d302801af535a58c207b33960b7cfdb116a933;hp=4b7664c224fdac212b9e5700b0fa800c74de4c73;hpb=df29cafb872244de1a6a9b3c273b329a6e15fa8c;p=helm.git diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml index 4b7664c22..6cbfeb1ff 100644 --- a/helm/ocaml/metadata/metadataDb.ml +++ b/helm/ocaml/metadata/metadataDb.ml @@ -76,7 +76,7 @@ let insert_const_no dbd uri = SELECT \"%s\",COUNT(DISTINCT h_occurrence) FROM %s WHERE NOT (h_position=\"%s\") AND (source = \"%s\")" - (conclno_hyp_tbl ()) uri (obj_tbl ()) inbody_pos uri + (fullno_tbl ()) uri (obj_tbl ()) inbody_pos uri in ignore (Mysql.exec dbd inconcl_no); ignore (Mysql.exec dbd concl_hyp) @@ -121,7 +121,7 @@ let index_inductive_def ~dbd = end let tables_to_clean = - [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl] + [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; fullno_tbl; name_tbl; hypno_tbl] let clean ~(dbd:Mysql.dbd) = let owned_uris = (* list of uris in list-of-columns format *)