From 2cd0ddf0c62f721ab5cb1b494b35e4eb3f19e2c9 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Fri, 20 Jan 2017 19:27:50 +0100 Subject: [PATCH] Hint database for iFrame. --- theories/proofmode/tactics.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v index 364a2b762..dbd4d3786 100644 --- 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. -- GitLab