-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