Notations do not always work in pattern-matching

[anton-trunov]

The following snippet produces an error message.

Require Import Coq.Lists.List.
Import ListNotations.
From Equations Require Import Equations.

Equations app {A} (l l' : list A) : list A :=
app [] l' := l' ;                                  (* <- here notations work *)
app (a :: l) l' := a :: (app l l').

The error message is

Error: Syntax error: ')' expected after [lpatt] (in [patt]).

It works if I change (a :: l) with cons a l.

Tested with Coq 8.8.0, Equations 1.0, both installed via OPAM.

[mattam82]

Yes, this is not easy to fix, I basically need to extend the pattern parser of Coq.

[mattam82]

This is now fixed in master, one can use notations freely in patterns.