From 787636f5e876c162b56c57ef6a5fa00c5249dba2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 7 Apr 2019 21:41:49 +0200
Subject: [PATCH] Avoid use of `firstorder`.

---
 theories/bi/big_op.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 7d61a954b..629d448a9 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -934,8 +934,8 @@ Section map2.
     - apply and_elim_r.
     - rewrite <- (left_id True%I (∧)%I (Φ i x1 x2)).
       apply and_mono=>//. apply pure_mono=>_ k.
-      rewrite !lookup_insert_is_Some' !lookup_empty.
-      firstorder.
+      rewrite !lookup_insert_is_Some' !lookup_empty -!not_eq_None_Some.
+      naive_solver.
   Qed.
 
   Lemma big_sepM2_fmap {A' B'} (f : A → A') (g : B → B') (Φ : nat → A' → B' → PROP) m1 m2 :
-- 
GitLab