diff --git a/tests/proofmode_siprop.v b/tests/proofmode_siprop.v index 1788f69c413a2ef2c7248efcc76014eff82af211..57e9a7332d47f12831d65ad23665ae0fb8eb953b 100644 --- a/tests/proofmode_siprop.v +++ b/tests/proofmode_siprop.v @@ -1,4 +1,4 @@ -From iris.proofmode Require Import tactics . +From iris.proofmode Require Import tactics. From iris.si_logic Require Import bi. Section si_logic_tests.