From 7fc6440b092573f8886c82320f28f9c1cf0f7d7c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 5 Sep 2021 13:13:52 -0400
Subject: [PATCH] remove an old leftover
---
theories/lang/lifting.v | 1 -
1 file changed, 1 deletion(-)
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index b67d3c12..997ba3f1 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -18,7 +18,6 @@ Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
num_laters_per_step _ := 0%nat;
state_interp_mono _ _ _ _ := fupd_intro _ _
}.
-Global Opaque iris_invGS.
Ltac inv_lit :=
repeat match goal with
--
GitLab