Commit 53ee592e authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers
Browse files

Apply 1 suggestion(s) to 1 file(s)

parent 104995c4
Pipeline #65927 passed with stage
in 8 minutes and 27 seconds
......@@ -291,8 +291,7 @@ Definition uPred_unseal :=
End restate.
(** New unseal tactic that also unfolds the BI layer.
This is used by [base_logic.algebra] and [base_logic.bupd_alt].
TODO: Can we get rid of this? *)
This is used by [base_logic.algebra] and [base_logic.bupd_alt]. *)
Ltac unseal := rewrite !uPred_unseal /=.
End uPred.
Supports Markdown
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