Writing intro_replacing in the new monad.
Enforcing the non-normalization of evars in Tactics.get_next_hyp_position.