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 ->
List.fold_right (build_term inductiveFuns) inductiveFuns
cic_body)
| CicNotationPt.Ident _
- | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
- | CicNotationPt.Ident (name, subst)
+ | CicNotationPt.Uri _
+ | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
+ | CicNotationPt.NRef _ -> assert false
+ | CicNotationPt.Ident (name,subst)
| CicNotationPt.Uri (name, subst) as ast ->
let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
(try