-let index_obj_for_auto status (uri, height, _, _, kind) =
- (*prerr_endline (string_of_int height);*)
- let mk_item orig_ty spec =
- let ty,_,_ = NCicMetaSubst.saturate ~delta:max_int [] [] [] orig_ty 0 in
- let keys =
- match ty with
- | NCic.Const (NReference.Ref (_,NReference.Def h))
- | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Def h))::_)
- when h > 0 ->
- let ty',_,_= NCicMetaSubst.saturate ~delta:(h-1) [] [] [] orig_ty 0 in
- [ty;ty']
- | _ -> [ty]
+let compute_keys status uri height kind =
+ let mk_item ty spec =
+ let orig_ty = NTacStatus.mk_cic_term [] ty in
+ let status,keys = NnAuto.keys_of_type status orig_ty in
+ let keys =
+ List.map
+ (fun t ->
+ snd (NTacStatus.term_of_cic_term status t (NTacStatus.ctx_of t)))
+ keys