+type 'term just =
+ [ `Term of 'term
+ | `Auto of 'term auto_params ]
+
+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
+ | NId of loc
+ | NIntro of loc * string
+ | NRewrite of loc * direction * CicNotationPt.term * npattern
+