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
| CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
| CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
| CicNotationPt.Sort (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
+ | CicNotationPt.Sort (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ()))
| CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
| CicNotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~mk_choice ~env