in
List.fold_left map g ss
| C.Cast (t1, t2) -> aux d (aux d g t2) t1
- | C.LetIn (_, t1, t2)
| C.Lambda (_, t1, t2)
| C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
+ | C.LetIn (_, t1, ty, t2) ->
+ aux d (aux d (aux (succ d) g t2) ty) t1
| C.MutCase (_, _, t1, t2, ss) ->
aux d (aux d (List.fold_left (aux d) g ss) t2) t1
| C.Fix (_, ss) ->
in
List.fold_left map g ss
| C.Cast (t1, t2) -> aux (aux g t2) t1
- | C.LetIn (_, t1, t2)
| C.Lambda (_, t1, t2)
- | C.Prod (_, t1, t2) -> aux (aux g t2) t1
+ | C.Prod (_, t1, t2) -> aux (aux g t2) t1
+ | C.LetIn (_, t1, ty, t2) -> aux (aux (aux g t2) ty) t1
| C.MutCase (_, _, t1, t2, ss) ->
aux (aux (List.fold_left aux g ss) t2) t1
| C.Fix (_, ss) ->
in
List.fold_left map (succ n) ss
| C.Cast (t1, t2)
- | C.LetIn (_, t1, t2)
| C.Lambda (_, t1, t2)
- | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1
+ | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1
+ | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (succ n) t2) ty) t1
| C.MutCase (_, _, t1, t2, ss) ->
aux (aux (List.fold_left aux (succ n) ss) t2) t1
| C.Fix (_, ss) ->