Commit a5eb66d3 authored by Ralf Jung's avatar Ralf Jung
Browse files

update a reference to long-gone double_neation module

parent ffacaa03
Pipeline #28221 passed with stage
in 21 minutes and 29 seconds
......@@ -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;
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment