diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v index 26a0cdb0c327290daab6f25e1c5b9f58535f3898..78602330d80580e115baffd2717ffca450eebf6d 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 :=