From a5eb66d356c52b080c35ad2746b725617c2a39d2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 14 May 2020 20:19:09 +0200
Subject: [PATCH] update a reference to long-gone double_neation module
---
theories/base_logic/bi.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 3b93a6e65..713caba78 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -217,7 +217,7 @@ End restate.
(** New unseal tactic that also unfolds the BI layer.
- This is used by [base_logic.double_negation].
+ This is used by [base_logic.bupd_alt].
TODO: Can we get rid of this? *)
Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_emp; simpl; unfold sbi_emp; simpl;
--
GitLab