From 3c5e3622b1cbefd3af20a83f6a2211d878a849b6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 12 Feb 2017 13:14:34 +0100
Subject: [PATCH] Remove another FIXME.
---
theories/typing/product_split.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 825605e6..4e90676d 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -24,7 +24,7 @@ Section product_split.
intros Hp.
revert off1 off2; induction tyl; intros off1 off2; simpl; first done.
rewrite !tctx_interp_cons. f_equiv; last first.
- { rewrite IHtyl plus_assoc. done. } (* FIXME RJ: Using assoc, even with a pattern, is pretty slow here. *)
+ { by rewrite IHtyl assoc_L. }
apply tctx_elt_interp_hasty_path. clear Hp. simpl.
clear. destruct (eval_path p); last done. destruct v; try done.
destruct l; try done. rewrite shift_loc_assoc Nat2Z.inj_add //.
--
GitLab