Verified Commit c75c0489 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Add (redundant?) test

Never used `Declare Instance`.
parent 40b36618
From iris.base_logic.lib Require Import invariants.
Instance test_cofe: Cofe (iPreProp Σ) := _.
Section tests.
Context `{!invG Σ}.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment