From 33f32edf2278232a5236181514aa9836b024450b Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 27 Feb 2019 17:12:42 -0500
Subject: Update a proof to work with previous commit

---
 src/UnderLetsProofs.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v
index 72c3ff53d..41bf801d2 100644
--- a/src/UnderLetsProofs.v
+++ b/src/UnderLetsProofs.v
@@ -351,9 +351,9 @@ Module Compilers.
 
         Lemma interp_splice_list {A B} (x : list (UnderLets A)) (e : list A -> UnderLets B)
           : interp (splice_list x e)
-            = interp (e (map interp x)).
+            = interp (e (List.map interp x)).
         Proof.
-          revert e; induction x as [|x xs IHx]; intros; cbn [splice_list interp map]; [ reflexivity | ].
+          revert e; induction x as [|x xs IHx]; intros; cbn [splice_list interp List.map]; [ reflexivity | ].
           rewrite interp_splice, IHx; reflexivity.
         Qed.
 
-- 
cgit v1.2.3