Test-suite for bug #3259.
Fix the behaviour of ML tactic notations w.r.t. Imports by making them
substitutive.