- | NCoercion of loc * string *
- NotationPt.term * NotationPt.term *
- (string * NotationPt.term) * NotationPt.term
- | NQed of loc
+ | NCoercion of loc * string * bool *
+ (nterm * nterm * (string * nterm) * nterm) option
+ | NQed of loc * bool
+ (* ex lexicon commands *)
+ | Alias of loc * alias_spec
+ (** parameters, name, type, fields *)
+ | Notation of loc * direction option * nterm * Gramext.g_assoc *
+ int * nterm
+ (* direction, l1 pattern, associativity, precedence, l2 pattern *)
+ | Interpretation of loc *
+ string * (string * NotationPt.argument_pattern list) *
+ NotationPt.cic_appl_pattern
+ (* description (i.e. id), symbol, arg pattern, appl pattern *)