-let cache_add_context ctx 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 key = CicSubstitution.lift i (head t) in
- let elem = Cic.Rel i in
- index acc key elem, i+1, tail ctx
- | Some (_,Cic.Def (_,Some t)) ->
- let key = CicSubstitution.lift i (head t) in
- let elem = Cic.Rel i in
- index acc key elem, i+1, tail ctx
- | Some (_,Cic.Def (t,None)) ->
- let ctx = tail ctx in
- let key,_ =
- CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph
- in
- let elem = Cic.Rel i in
- let key = CicSubstitution.lift i (head key) in
- index acc key elem, i+1, ctx
- | _ -> acc,i+1,tail ctx)
- (cache,1,ctx) ctx