in
let cic_body =
aux ~localize loc context' (add_binders `Lambda body) in
+ let typ =
+ match typ with
+ Some typ -> typ
+ | None-> CicNotationPt.Implicit `JustOne 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 ->
with
CicEnvironment.CircularDependency _ ->
raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
- | CicNotationPt.Implicit -> Cic.Implicit None
+ | CicNotationPt.Implicit `Vector -> assert false
+ | CicNotationPt.Implicit (`JustOne | `Tagged _) -> Cic.Implicit None
| CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
| CicNotationPt.Num (num, i) ->
Disambiguate.resolve ~mk_choice ~env
(fun (context,res) (name,t) ->
let t =
match t with
- None -> CicNotationPt.Implicit
+ None -> CicNotationPt.Implicit `JustOne
| Some t -> t in
let name = CicNotationUtil.cic_name_of_name name in
name::context,(name, interpretate_term context env None false t)::res
(fun (context,res) (name,t) ->
let t =
match t with
- None -> CicNotationPt.Implicit
+ None -> CicNotationPt.Implicit `JustOne
| Some t -> t in
let name = CicNotationUtil.cic_name_of_name name in
name::context,(name, interpretate_term context env None false t)::res