- CicNotationPt.fail loc "Ill formed reference")
- | CicNotationPt.NRef nref -> NCic.Const nref
- | 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)
- | CicNotationPt.UserInput -> NCic.Implicit `Hole
- | CicNotationPt.Num (num, i) ->
+ NotationPt.fail loc "Ill formed reference")
+ | NotationPt.NRef nref -> NCic.Const nref
+ | NotationPt.NCic t -> t
+ | NotationPt.Implicit `Vector -> NCic.Implicit `Vector
+ | NotationPt.Implicit `JustOne -> NCic.Implicit `Term
+ | NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
+ | NotationPt.UserInput -> NCic.Implicit `Hole
+ | NotationPt.Num (num, i) ->