- if !level = 2 then begin
- let id =
- CicNotationParser.extend ~precedence:50 ~associativity:Gramext.LeftA
- (P.Layout (P.Box (P.H,
- [
- P.Magic
- (P.List1
- (P.Layout (P.Box (P.H,
- [ P.Literal (`Symbol "|");
- P.Variable (P.TermVar "ugo");
- P.Magic (P.Opt (P.Layout (P.Box (P.H,
- [ P.Literal (`Symbol ",");
- P.Variable (P.TermVar "pino")]))));
- P.Literal (`Symbol "|");
- ])),
- Some (`Symbol ";")));
-(* P.Literal (`Symbol "+");
- P.Magic (P.Opt (P.Layout (P.Box (P.H,
- [
- P.Variable (P.TermVar "ugo");
- P.Literal (`Symbol "+");
- P.Variable (P.TermVar "pino")
- ])))); *)
-(* P.Variable (P.TermVar "a");
- P.Literal (`Symbol "+");
- P.Variable (P.TermVar "b"); *)
- ])))
- (fun env _ ->
- prerr_endline "reducing rule" ;
- prerr_endline (sprintf "env = [ %s ]" (CicNotationPp.pp_env env));
- P.Sort `Prop)
- in
- CicNotationParser.print_l2_pattern ()
- end;