From e17646915543510d905daaeb0019600242e1dbc9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 12 Jul 2017 20:38:38 +0200
Subject: [PATCH] Fix typo.

---
 theories/proofmode/class_instances.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 6586c849b..23fd37412 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -392,7 +392,7 @@ Proof. intros. by rewrite /FromAnd big_opL_app always_and_sep_l. Qed.
 (* 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').
+  IsOp a b1 b2 → IsOp a' b1' b2' → IsOp' (a,a') (b1,b1') (b2,b2').
 Proof. by constructor. Qed.
 Global Instance is_op_pair_persistent_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
   Persistent a → IsOp a' b1' b2' → IsOp' (a,a') (a,b1') (a,b2').
-- 
GitLab