(*assert (not (is_main_pos pos));*)
let set = aux (next_pos pos) set source in
aux (next_pos pos) set target
- | Cic.LetIn (_, term, target) ->
+ | Cic.LetIn (_, term, _, target) ->
if is_main_pos pos then
aux pos set (CicSubstitution.subst term target)
else
| Cic.Lambda (_, source, target) ->
let acc = aux in_hyp acc source in
aux in_hyp acc target
- | Cic.LetIn (_, term, target) ->
+ | Cic.LetIn (_, term, _, target) ->
aux in_hyp acc (CicSubstitution.subst term target)
| Cic.Appl [] -> assert false
| Cic.Appl (hd :: tl) ->