+ (* ex lexicon commands *)
+ | Alias of loc * alias_spec
+ (** parameters, name, type, fields *)
+ | Notation of loc * direction option * NotationPt.term * Gramext.g_assoc *
+ int * NotationPt.term
+ (* 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 *)