+let basic_index_obj l status =
+ status#set_auto_cache
+ (List.fold_left
+ (fun t (k,v) ->
+ NDiscriminationTree.DiscriminationTree.index t k v)
+ status#auto_cache l)
+;;
+
+let record_index_obj =
+ let aux l
+ ~refresh_uri_in_universe
+ ~refresh_uri_in_term
+ =
+ basic_index_obj
+ (List.map
+ (fun k,v -> refresh_uri_in_term k, refresh_uri_in_term v)
+ l)
+ in
+ NCicLibrary.Serializer.register#run "index_obj"
+ object(_ : 'a NCicLibrary.register_type)
+ method run = aux
+ end
+;;
+
+let index_obj_for_auto status (uri, height, _, _, kind) =
+ let data =
+ match kind with
+ | NCic.Fixpoint _ -> []
+ | NCic.Inductive _ -> []
+ | NCic.Constant (_,_,Some _, ty, _) ->
+ let ty,_,_ = NCicMetaSubst.saturate [] [] [] ty 0 in
+ [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Def height))]
+ | NCic.Constant (_,_,None, ty, _) ->
+ let ty,_,_ = NCicMetaSubst.saturate [] [] [] ty 0 in
+ [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Decl))]
+ in
+ let status = basic_index_obj data status in
+ let dump = record_index_obj data :: status#dump in
+ status#set_dump dump
+;;
+
+