You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
revert
may revertimplDetail
hypotheses 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 turnimplDetail
hypotheses into regular hypotheses. I don't expect this to get fixed in core since core doesn't useimplDetail
hypotheses in this way, so we should make sure that rules never receive goals withimplDetail
hypotheses.The text was updated successfully, but these errors were encountered: