find_image_aux (what,with_what)
in
let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
- let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in
+ let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in
let rec substaux k ctx what t =
try
S.lift (k-1) (find_image ctx what t)
| C.Lambda (n,s,t) ->
C.Lambda
(n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
C.LetIn
- (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t)
+ (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t)
| C.Appl (he::tl) ->
(* Invariant: no Appl applied to another Appl *)
let tl' = List.map (substaux k ctx what) tl in