diff --git a/tests/siprop.v b/tests/siprop.v index da5fc4be47da6a3e853dc5967b065a8f5993e494..fc72d0ccce2bfc8f9b98adb2786bcbb09867b22f 100644 --- a/tests/siprop.v +++ b/tests/siprop.v @@ -2,4 +2,4 @@ From iris.si_logic Require Import bi. (** Make sure that [siProp]s are parsed in [bi_scope]. *) Definition test : siProp := â–· True. -Definition testI : siPropI := â–· True. \ No newline at end of file +Definition testI : siPropI := â–· True.