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