From c75c048938c33699ef8c34ff1cdb24f99e884381 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Thu, 16 May 2019 14:09:12 +0200
Subject: [PATCH] Add (redundant?) test

Never used `Declare Instance`.
---
 tests/algebra.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tests/algebra.v b/tests/algebra.v
index 028272ce..5dd2e68a 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 Σ}.
 
-- 
GitLab