| Include of loc * inclusion_mode * string (* _,buri,_,path *)
| UnificationHint of loc * NotationPt.term * int (* term, precedence *)
| NObj of loc * NotationPt.term NotationPt.obj
| Include of loc * inclusion_mode * string (* _,buri,_,path *)
| UnificationHint of loc * NotationPt.term * int (* term, precedence *)
| NObj of loc * NotationPt.term NotationPt.obj