Notations with binders and ltac2:(...) are unusable

[andres-erbsen]

Description of the problem

From Ltac2 Require Import Ltac2.
Notation "bleh! { x , P }" := (let f := fun x => P in ltac2:(exact tt)).
Notation "blehs! { x .. y , p }" :=
  (let t := ex (fun x => .. (ex (fun y => p)) ..) in ltac2:(exact tt)) (x binder).
Check bleh! { x , True }. (* Missing notation term for variable x, probably an ill-typed expression *)
Check blehs! { a b c , True }. (* Missing notation term for variables x y, probably an ill-typed expression *)

Coq Version

8.15.0, 8.16.0

[samuelgruetter]

If I add (x binder) to the non-recursive notation, it works, so the problems seems to be specific to recursive notations?

[samuelgruetter]

A similar issue also appears with Ltac1: #7903