in
let cic_body =
aux ~localize loc context' (add_binders `Lambda body) in
+ let typ =
+ match typ with Some typ -> typ | None-> CicNotationPt.Implicit in
let cic_type =
aux_option ~localize loc context (Some `Type)
- (HExtlib.map_option (add_binders `Pi) typ) in
+ (Some (add_binders `Pi typ)) in
let name =
match CicNotationUtil.cic_name_of_name name with
| Cic.Anonymous ->