Ltac unification variable containing locally-bound variables

Question

The Ltac chapter of CPDT, shows a "faulty" tactic:

Theorem t1' : forall x : nat, x = x.
  match goal with
    | [ |- forall x, ?P ] => trivial
  end.

The book then explains

The problem is that unification variables may not contain locally bound variables.
In this case, [?P] would need to be bound to [x = x], which contains the local quantified
variable [x].  By using a wildcard in the earlier version, we avoided this restriction.

However, the tactic above actually works in Coq 8.11!

Can unification variables now contain locally-bound variables? If so, is there any difference between the above and

Theorem t1' : forall x : nat, x = x.
  match goal with
    | [ |- forall x, _ ] => trivial
  end.

(where we replaced ?P by _)?

Answer 1

The difference between ?P and _ is that you can actually refer to P in the branch. Unfortunately, P is an open term, so it might quickly end up being ill-formed, so there is not much you can do with it. So, I would not rely on it. It is better to use forall x, @?P x as a pattern, so that P is a closed term.

Answer 2

The book provides some more info later on:

Actually, the behavior demonstrated here applies to Coq version 8.4,
but not 8.4pl1.  The latter version will allow regular Ltac pattern
variables to match terms that contain locally bound variables, but a
tactic failure occurs if that variable is later used as a Gallina term.

This means that in

Ltac dummy :=
  match goal with
  | [ H: forall x, ?P |- _ ] => assert True
  end.

Lemma foo (a x : nat) :
  (forall n, n = 42) ->  
  True.
Proof.
  intros.
  dummy.

the dummy tactic can be applied (because we match ?P but don't refer to it later on), but if we change dummy to be

Ltac dummy :=
  match goal with
  | [ H: forall x, ?P |- _ ] => assert ?P
  end.

then that'll fail because we're referring to ?P, which is potentially an open term.