Commit 5ea75b53 authored by Ralf Jung's avatar Ralf Jung

experiment with removing an instance

parent 6aed7177
......@@ -3,6 +3,8 @@ From iris.algebra Require Import updates local_updates.
From stdpp Require Export sets gmap mapset.
Set Default Proof Using "Type".
Remove Hints set_unfold_elements : typeclass_instances.
(* The union CMRA *)
Section gset.
Context `{Countable K}.
......
......@@ -3,6 +3,8 @@ From iris.bi Require Export big_op.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Remove Hints set_unfold_elements : typeclass_instances.
Section lifting.
Context `{!irisG Λ Σ}.
Implicit Types v : val Λ.
......
Markdown is supported
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