From 2ea5d210bdae9fe5c19633ef3660b5e37c3867c6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 5 Oct 2016 22:51:56 +0200
Subject: [PATCH] IntoOp and FromOp instances for the authoritative fragment.

---
 algebra/auth.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/algebra/auth.v b/algebra/auth.v
index cd2a8b326..d831c6081 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export excl local_updates.
 From iris.algebra Require Import upred updates.
+From iris.proofmode Require Import class_instances.
 Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
 
@@ -224,6 +225,14 @@ End cmra.
 Arguments authR : clear implicits.
 Arguments authUR : clear implicits.
 
+(* Proof mode class instances *)
+Instance from_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
+  FromOp a b1 b2 → FromOp (◯ a) (◯ b1) (◯ b2).
+Proof. done. Qed.
+Instance into_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
+  IntoOp a b1 b2 → IntoOp (◯ a) (◯ b1) (◯ b2).
+Proof. done. Qed.
+
 (* Functor *)
 Definition auth_map {A B} (f : A → B) (x : auth A) : auth B :=
   Auth (excl_map f <$> authoritative x) (f (auth_own x)).
-- 
GitLab