let process_notation st =
match st with
| Notation (loc, dir, l1, associativity, precedence, l2) ->
+ let l1 =
+ CicNotationParser.check_l1_pattern l1 precedence associativity
+ in
let item = (l1, precedence, associativity, l2) in
let rule_id = ref [] in
let _ =
if dir <> Some `RightToLeft then
let create_cb (l1, precedence, associativity, l2) =
let id =
- CicNotationParser.extend l1 ?precedence ?associativity
+ CicNotationParser.extend l1
(fun env loc ->
CicNotationPt.AttributedTerm
(`Loc loc,TermContentPres.instantiate_level2 env l2)) in
let pp_id =
if dir <> Some `LeftToRight then
[ PrettyPrinterId
- (TermContentPres.add_pretty_printer ?precedence ?associativity
+ (TermContentPres.add_pretty_printer
l2 l1) ]
else
[]