From b9af598b55b5cb8afdd525d10c406145b2278de9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 1 Jun 2018 12:14:05 +0200
Subject: [PATCH] port tweak from gen_proofmode branch

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

diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 26a0cdb0..78602330 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -19,8 +19,8 @@ Global Opaque iris_invG.
 
 Ltac inv_lit :=
   repeat match goal with
-  | H : lit_eq _ ?x ?y |- _ => inversion H; clear H; simplify_eq/=
-  | H : lit_neq ?x ?y |- _ => inversion H; clear H; simplify_eq/=
+  | H : lit_eq _ ?x ?y |- _ => inversion H; clear H; simplify_map_eq/=
+  | H : lit_neq ?x ?y |- _ => inversion H; clear H; simplify_map_eq/=
   end.
 
 Ltac inv_bin_op_eval :=
-- 
GitLab