negative integers not accepted in ltac integer_list -- same bug on coq 8.11.1

[moninje]

Description of the problem

pattern n at -2 works, but not when called within a yser-defined tactic.

Definition MARQ {A: Type} (x:A) := x.
Tactic Notation "mark" constr(P) "at" integer_list(L) :=
pattern P at L;
match goal with |- ?f ?x => change (f (MARQ x)) end;
cbv beta.
Goal forall n, n + n = n + n.
intro n.
mark n at 2 3.
Undo 1.
pattern n at -2.
Undo 1.
mark n at -2.
(* Error:
Anomaly
"Uncaught exception File "pretyping/find_subterm.ml", line 57, characters 4-10: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
*)

Coq Version

8.9.0

[moninje]

The first example was unnecessarily long, here is a minimal version in 3 lines.
Same bug on 8.9.0 and 8.11.1

Tactic Notation "mark" constr(P) "at" integer_list(L) := pattern P at L.
Goal 0 = 0.
mark 0 at -2.

[proux01]

Thanks @moninje for reporting and sorry for the late answer. This is fixed in master. The fix should land in 8.12.