if localize then
match body with
CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
+ (* 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
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