Commit 92856938 authored by Robbert Krebbers's avatar Robbert Krebbers

iModIntro hint for U.

parent d0b89ea5
......@@ -79,3 +79,5 @@ Section U.
Global Instance from_modal_later P : FromModal modality_U (U P) (U P) P.
Proof. by rewrite /FromModal. Qed.
End U.
Hint Extern 1 (environments.envs_entails _ (U _)) => iModIntro.
\ No newline at end of file
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment