revert may revert implDetail hypotheses if they depend on one of the (regular) hypotheses to be reverted. As a result, tactics which are implemented in terms of revert, such as subst, can inadvertently turn implDetail hypotheses into regular hypotheses. I don't expect this to get fixed in core since core doesn't use implDetail hypotheses in this way, so we should make sure that rules never receive goals with implDetail hypotheses.
revertmay revertimplDetailhypotheses if they depend on one of the (regular) hypotheses to be reverted. As a result, tactics which are implemented in terms ofrevert, such assubst, can inadvertently turnimplDetailhypotheses into regular hypotheses. I don't expect this to get fixed in core since core doesn't useimplDetailhypotheses in this way, so we should make sure that rules never receive goals withimplDetailhypotheses.