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
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