How to add variables introduced by set tactic to a Hint DB?

Question

I want to use a Hint DB with variables introduced by set. For example,

Example foo : forall n : nat, n + n = n + n.forall n : nat, n + n = n + n
Proof.forall n : nat, n + n = n + n
  intro.n: nat
n + n = n + n
  set (m := n + n).n: nat
m:= n + n: nat
m = m
#[local] Hint Unfold m : core.The reference m was not found in the current
environment.

Is there any way to achieve this, or is it impossible?

Answer

It's not possible to do this like you suggested because after you finish foo with Qed the local variable m will be out of scope, but hints go straight into some global database.

However, you can use the Section mechanism, as the hints declared inside a section are local to that section:

Section LocalHints.
  Variable n : nat.
  Let m := n + n.
  Hint Unfold m.Adding and removing hints in the core database
implicitly is deprecated. Please specify a hint
database. [implicit-core-hint-db,deprecated]

  Example bar : m = m.n: nat
m:= n + n: nat
m = m
  Proof.n: nat
m:= n + n: nat
m = m
    autounfold with core.n: nat
m:= n + n: nat
n + n = n + n
    reflexivity.
  Qed.
End LocalHints.