+ | CicNotationPt.NCic t ->
+ let context = (* to make metas_of_term happy *)
+ List.map (fun x -> x,NCic.Decl (NCic.Implicit `Type)) context in
+ assert(NCicUntrusted.metas_of_term [] context t = []); t
+ | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
+ | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
+ | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)