Hint database for iFrame.

2cd0ddf0 · Robbert Krebbers · 98f73a0b · 2cd0ddf0
Commit 2cd0ddf0 authored Jan 20, 2017 by Robbert Krebbers
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1322,3 +1322,5 @@ Hint Extern 1 (of_envs _ ⊢ |==> _) => iModIntro.
 Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro.
 Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iLeft.
 Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iRight.
+
+Hint Extern 2 (coq_tactics.of_envs _ ⊢ _ ∗ _) => progress iFrame : iFrame.