Notation variables are now taken into account as possible ltac bound variables
when internalizing a term.