From e9d8df762e8c07c64ed37b3c7917ba3be79794c5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 1 Jan 2017 14:58:27 +0100
Subject: [PATCH] Remove another FIXME.

Note that the _L lemmas/class projections are always faster (and
prefered to be used) when possible.
---
 theories/typing/type.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/typing/type.v b/theories/typing/type.v
index 004b4433..823bed72 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -88,7 +88,7 @@ Section type.
     (n ≤ m)%nat → shr_locsE l n ⊆ shr_locsE l m.
   Proof.
     induction 1; first done.
-    rewrite ->IHle. rewrite -Nat.add_1_l [(_ + _)%nat]comm.  (* FIXME last rewrite is very slow. *)
+    rewrite ->IHle. rewrite -Nat.add_1_l [(_ + _)%nat]comm_L.
     rewrite shr_locsE_shift. set_solver+.
   Qed.
 
-- 
GitLab