+type ntactic =
+ | NApply of loc * CicNotationPt.term
+ | NCases of loc * CicNotationPt.term * npattern
+ | NCase1 of loc * string
+ | NChange of loc * npattern * CicNotationPt.term
+ | NElim of loc * CicNotationPt.term * npattern
+ | NEval of loc * npattern * [ `Whd of bool ]
+ | NGeneralize of loc * npattern
+ | NId of loc
+ | NIntro of loc * string
+ | NRewrite of loc * direction * CicNotationPt.term * npattern
+