let add_obj uri obj status =
let dbd = MatitaDb.instance () in
let suri = UriManager.string_of_uri uri in
if CicEnvironment.in_library uri then
command_error (sprintf "%s already defined" suri)
else begin
let add_obj uri obj status =
let dbd = MatitaDb.instance () in
let suri = UriManager.string_of_uri uri in
if CicEnvironment.in_library uri then
command_error (sprintf "%s already defined" suri)
else begin