if localize then
match body with
CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
- let l' = List.map (aux ~localize loc context) l in
+ let l' = List.map (aux ~localize loc context') l in
`AvoidLetIn (n,l')
| _ -> assert false
else
CicNotationUtil.cic_name_of_name var :: context,
domain_of_term_option ~loc ~context ty @ res)
(add_defs context,[]) params))
+ @ dom
@ domain_of_term_option ~loc ~context:context' typ
@ domain_of_term ~loc ~context:context' body
) [] defs