with NRef.IllFormedReference _ ->
CicNotationPt.fail loc "Ill formed reference")
| CicNotationPt.NRef nref -> NCic.Const nref
- | CicNotationPt.Implicit -> NCic.Implicit `Term
+ | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
+ | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
| CicNotationPt.UserInput -> NCic.Implicit `Hole
| CicNotationPt.Num (num, i) ->
Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
res
| Some (CicNotationPt.AttributedTerm (_, term)) ->
aux_option ~localize loc context annotation (Some term)
- | Some CicNotationPt.Implicit -> NCic.Implicit annotation
+ | Some CicNotationPt.Implicit `JustOne -> NCic.Implicit annotation
+ | Some CicNotationPt.Implicit `Vector -> assert false
| Some term -> aux ~localize loc context term
in
(fun ~context -> aux ~localize:true HExtlib.dummy_floc context),
(fun (context,res) (name,t) ->
let t =
match t with
- None -> CicNotationPt.Implicit
+ None -> CicNotationPt.Implicit `JustOne
| Some t -> t in
let name = cic_name_of_name name in
let t =
(fun (context,res) (name,t) ->
let t =
match t with
- None -> CicNotationPt.Implicit
+ None -> CicNotationPt.Implicit `JustOne
| Some t -> t in
let name = cic_name_of_name name in
let t =