if localize then
match body with
CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
- let l' = List.map (aux ~localize loc context') l in
+ (* since we avoid the letin, the context has no
+ * recfuns in it *)
+ let l' = List.map (aux ~localize loc context) l in
`AvoidLetIn (n,l')
| _ -> assert false
else