-let compute_keys uri height kind =
- let mk_item orig_ty spec =
- let keys = NnAuto.keys_of_cic_term [] [] [] orig_ty in
+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
+ in