From 6f23defb5fe22da45fa96114fd07999ff672b905 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 11 Jan 2017 14:01:22 +0100
Subject: [PATCH] Remove FIXME that is no longer needed in current 8.6.

---
 theories/algebra/gmap.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index b3f13832c..5eae3b896 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -146,8 +146,7 @@ Proof.
   - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
     by rewrite -lookup_op.
   - intros n m. induction m as [|i x m Hi IH] using map_ind=> m1 m2 Hmv Hm.
-    { exists ∅. exists ∅. (* FIXME: exists ∅, ∅. results in a TC loop in Coq 8.6 *)
-      split_and!=> -i; symmetry; symmetry in Hm; move: Hm=> /(_ i);
+    { exists ∅, ∅. split_and!=> -i; symmetry; symmetry in Hm; move: Hm=> /(_ i);
         rewrite !lookup_op !lookup_empty ?dist_None op_None; intuition. }
     destruct (IH (delete i m1) (delete i m2)) as (m1'&m2'&Hm'&Hm1'&Hm2').
     { intros j; move: Hmv=> /(_ j). destruct (decide (i = j)) as [->|].
-- 
GitLab