let obj = Cic.Constant (name, body, ty, params, attrs) in
let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
CicEnvironment.add_type_checked_term uri (obj, ugraph);
- MetadataDb.index_constant ~dbd ~uri ~body ~ty;
+ MetadataDb.index_obj ~dbd ~uri; (* must be in the env *)
let new_stuff = save_object_to_disk status uri obj in
MatitaLog.message (sprintf "%s constant defined" suri);
{ status with objects = new_stuff @ status.objects }
let obj = Cic.InductiveDefinition (types, params, leftno, attrs) in
let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
CicEnvironment.put_inductive_definition uri (obj, ugraph);
- MetadataDb.index_inductive_def ~dbd ~uri ~types:types;
+ MetadataDb.index_obj ~dbd ~uri; (* must be in the env *)
let new_stuff = save_object_to_disk status uri obj in
MatitaLog.message (sprintf "%s inductive type defined" suri);
let status = { status with objects = new_stuff @ status.objects } in