- | Notation of loc * 'term * Gramext.g_assoc option * int option * 'term
- (* level 1 pattern, associativity, precedence, level 2 pattern *)
- | Interpretation of loc * (string * argument_pattern list) * cic_appl_pattern
+ | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc *
+ int * CicNotationPt.term
+ (* direction, l1 pattern, associativity, precedence, l2 pattern *)
+ | Interpretation of loc *
+ string * (string * CicNotationPt.argument_pattern list) *
+ CicNotationPt.cic_appl_pattern
+ (* description (i.e. id), symbol, arg pattern, appl pattern *)