Tactics in terms in notations break binders / open term

#### Version

8.8.0

#### Description of the problem

```coq
Notation foo x f := (fun x : nat => f).
Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)).
Check foo x (x + x). (* success *)
Check bar x (x + x). (* Error: The reference x was not found in the current environment. *)
```

See also #5696, #3304, #3468

cc @herbelin , @ppedrot , @andres-erbsen