Fix the behaviour of ML tactic notations w.r.t. Imports by making them
substitutive.