- | UnificationHint of loc * NotationPt.term * int (* term, precedence *)
- | NObj of loc * NotationPt.term NotationPt.obj
- | NDiscriminator of loc * NotationPt.term
- | NInverter of loc * string * NotationPt.term * bool list option * NotationPt.term option
+ | UnificationHint of loc * nterm * int (* term, precedence *)
+ | NObj of loc * nterm NotationPt.obj * bool
+ | NDiscriminator of loc * nterm
+ | NInverter of loc * string * nterm * bool list option * nterm option