diff --git a/tests/algebra.v b/tests/algebra.v index 028272cea5e582c85243c312e6582241c13e5648..5dd2e68aa47501844664db73a4af79c35472f566 100644 --- a/tests/algebra.v +++ b/tests/algebra.v @@ -1,5 +1,7 @@ From iris.base_logic.lib Require Import invariants. +Instance test_cofe: Cofe (iPreProp Σ) := _. + Section tests. Context `{!invG Σ}.