-let cache_add_context context metasenv cache =
- let tail = function [] -> [] | h::tl -> tl in
- let rc,_,_ =
- List.fold_left
- (fun (acc,i,ctx) ctxentry ->
- match ctxentry with
- | Some (_,Cic.Decl t) ->
- let ty = CicSubstitution.lift i t in
- let elem = Cic.Rel i in
- index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
- (* index acc key elem, i+1, tail ctx *)
- | Some (_,Cic.Def (_,Some t)) ->
- let ty = CicSubstitution.lift i t in
- let elem = Cic.Rel i in
- index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
- | Some (_,Cic.Def (t,None)) ->
- let ctx = tail ctx in
- let ty =
- CicSubstitution.lift i
- (fst (CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph))
- in
- let elem = Cic.Rel i in
- index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
- | _ -> acc,i+1,tail ctx)
- (cache,1,context) context
+
+let cache_add_list (univ,cache) context terms_and_types =
+ let univ =
+ List.fold_left
+ (fun univ (t,ty) ->
+ prerr_endline ("indexing: " ^ CicPp.ppterm ty);
+ Universe.index_local_term univ context t ty)
+ univ terms_and_types