diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v index 186e1dda9de6d9552afec1fad762585aca62fffb..37eaf0a8c56540284b202d24f8f7a44b86057606 100644 --- a/theories/proofmode/tactics.v +++ b/theories/proofmode/tactics.v @@ -1903,5 +1903,4 @@ Hint Extern 1 (envs_entails _ (_ ∨ _)) => iRight. Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro. Hint Extern 2 (envs_entails _ (|={_}=> _)) => iModIntro. - Hint Extern 2 (envs_entails _ (_ ∗ _)) => progress iFrame : iFrame.