Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it
exhibits the "useless goal" behaviour: there is code out there depending on
the fact that goals cannot be solved by side effects.