From bd60eade3e7467623af8f627c4e3af02e888acc8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 May 2018 12:10:01 +0200
Subject: [PATCH] Move generic `IsOp` instances to
 `algebra/proofmode_classes.v`.

---
 theories/algebra/proofmode_classes.v | 23 ++++++++++++++++++++++-
 theories/base_logic/base_logic.v     | 21 ---------------------
 2 files changed, 22 insertions(+), 22 deletions(-)

diff --git a/theories/algebra/proofmode_classes.v b/theories/algebra/proofmode_classes.v
index 1c033303b..7ccebbe78 100644
--- a/theories/algebra/proofmode_classes.v
+++ b/theories/algebra/proofmode_classes.v
@@ -30,4 +30,25 @@ Class IsOp'LR {A : cmraT} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
 Existing Instance is_op_lr | 0.
 Hint Mode IsOp'LR + ! - - : typeclass_instances.
 Instance is_op_lr_op {A : cmraT} (a b : A) : IsOp'LR (a â‹… b) a b | 0.
-Proof. by rewrite /IsOp'LR /IsOp. Qed.
\ No newline at end of file
+Proof. by rewrite /IsOp'LR /IsOp. Qed.
+
+(* FromOp *)
+(* TODO: Worst case there could be a lot of backtracking on these instances,
+try to refactor. *)
+Global Instance is_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
+  IsOp a b1 b2 → IsOp a' b1' b2' → IsOp' (a,a') (b1,b1') (b2,b2').
+Proof. by constructor. Qed.
+Global Instance is_op_pair_core_id_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
+  CoreId a → IsOp a' b1' b2' → IsOp' (a,a') (a,b1') (a,b2').
+Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
+Global Instance is_op_pair_core_id_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
+  CoreId a' → IsOp a b1 b2 → IsOp' (a,a') (b1,a') (b2,a').
+Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
+
+Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
+  IsOp a b1 b2 → IsOp' (Some a) (Some b1) (Some b2).
+Proof. by constructor. Qed.
+(* This one has a higher precendence than [is_op_op] so we get a [+] instead of
+an [â‹…]. *)
+Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
+Proof. done. Qed.
\ No newline at end of file
diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index edcc029b4..3fd684dca 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -37,27 +37,6 @@ Proof.
   rewrite -cmra_valid_intro //. by apply pure_intro.
 Qed.
 
-(* FromOp *)
-(* TODO: Worst case there could be a lot of backtracking on these instances,
-try to refactor. *)
-Global Instance is_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
-  IsOp a b1 b2 → IsOp a' b1' b2' → IsOp' (a,a') (b1,b1') (b2,b2').
-Proof. by constructor. Qed.
-Global Instance is_op_pair_core_id_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
-  CoreId  a → IsOp a' b1' b2' → IsOp' (a,a') (a,b1') (a,b2').
-Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
-Global Instance is_op_pair_core_id_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
-  CoreId a' → IsOp a b1 b2 → IsOp' (a,a') (b1,a') (b2,a').
-Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
-
-Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
-  IsOp a b1 b2 → IsOp' (Some a) (Some b1) (Some b2).
-Proof. by constructor. Qed.
-(* This one has a higher precendence than [is_op_op] so we get a [+] instead of
-an [â‹…]. *)
-Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
-Proof. done. Qed.
-
 Global Instance from_sep_ownM (a b1 b2 : M) :
   IsOp a b1 b2 →
   FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-- 
GitLab