X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2Ftest.ml;fp=helm%2Focaml%2Fmetadata%2Ftest.ml;h=8e805840a499e1460637d029a83e787ab1228dcd;hb=26c3b57c2142bfd2242571109374c3203c7980dd;hp=21274a585e37020c4652a1f865439191e8f3b9ed;hpb=49e1d8c87e52b9b62bad467246e953d3af81a692;p=helm.git

diff --git a/helm/ocaml/metadata/test.ml b/helm/ocaml/metadata/test.ml
index 21274a585..8e805840a 100644
--- a/helm/ocaml/metadata/test.ml
+++ b/helm/ocaml/metadata/test.ml
@@ -8,7 +8,7 @@ in
 let owner =
   try
     Sys.argv.(2)
-  with Invalid_argument _ -> "matita_test"
+  with Invalid_argument _ -> "matita_test2"
 in
 let _ = MetadataTypes.ownerize_tables owner in
 if Sys.argv.(1) = "clean" then begin
@@ -24,14 +24,7 @@ end else
       incr n;
       Printf.printf "%d\t%s\n" !n line; flush stdout;
       let uri = UriManager.uri_of_string line in
-      (match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
-      | Cic.Constant (_, body, ty, _, _), _ ->
-          MetadataDb.index_constant ~body ~ty ~uri ~dbd
-      | Cic.Variable (_, body, ty, _, _), _ ->
-          MetadataDb.index_constant ~body ~ty ~uri ~dbd
-      | Cic.InductiveDefinition (types, _, _, _), _ ->
-          MetadataDb.index_inductive_def ~dbd ~uri ~types
-      | _ -> assert false)
+      MetadataDb.index_obj ~dbd ~uri
     done
   with End_of_file -> close_in ic