let _ = Helm_registry.set "getter.mode" "remote"; let _ = Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/" in let dbd = Mysql.quick_connect ~host:"mowgli.cs.unibo.it" ~user:"helm" ~database:"matita" () in let owner = try Sys.argv.(2) with Invalid_argument _ -> "matita_test" in if Sys.argv.(1) = "clean" then MetadataDb.clean ~dbd ~owner else let uri_str = Sys.argv.(1) in let uri = UriManager.uri_of_string uri_str in match CicEnvironment.get_obj uri with | Cic.Constant (_, body, ty, _) -> MetadataDb.index_constant ~body ~ty ~uri ~owner ~dbd | Cic.InductiveDefinition (types, _, _) -> MetadataDb.index_inductive_def ~dbd ~owner ~uri ~types | _ -> assert false