diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v index b67d3c12c6ea524abb70d60a18d64406b084eeb4..997ba3f1b3f2c7056870fd48e7b30dfb4571098f 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