From 6b68b1716d0b3b89395995665625d165d2f6f6bd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 11 Jun 2017 13:57:15 +0200
Subject: [PATCH] Add is_op_plus to make iCombine behave nicer for nat.

---
 theories/proofmode/class_instances.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 869e6e084..6586c849b 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -404,6 +404,10 @@ Proof. constructor=> //=. by rewrite -persistent_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.
 
 (* IntoAnd *)
 Global Instance into_and_sep p P Q : IntoAnd p (P ∗ Q) P Q.
-- 
GitLab