Commit 985f9713 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Add hint for introducing absorbingly.

parent e5c69b43
......@@ -1984,6 +1984,7 @@ Hint Extern 1 (envs_entails _ (◇ _)) => iModIntro.
Hint Extern 1 (envs_entails _ (_ _)) => iLeft.
Hint Extern 1 (envs_entails _ (_ _)) => iRight.
Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro.
Hint Extern 1 (envs_entails _ (<absorb> _)) => iModIntro.
Hint Extern 2 (envs_entails _ (|={_}=> _)) => iModIntro.
Hint Extern 2 (envs_entails _ (_ _)) => progress iFrame : iFrame.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment