Commit 616f81e7 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'robbert/disclaimer_sts' into 'master'

Disclaimer for STSs.

See merge request !366
parents f7f0a171 a21e0baf
Pipeline #23380 passed with stage
in 18 minutes and 11 seconds
......@@ -6,6 +6,12 @@ Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments core _ _ !_ /.
(** DISCLAIMER: The definition of STSs is included in the Iris development for
historical purposes. If you plan to mechanize an Iris proof in Coq, it is
usually better to use a more direct encoding of the ghost state you need as a
resource algebra (camera). STSs are very painful to use in Coq, and they are
therefore barely used in practice. *)
(** * Definition of STSs *)
Module sts.
Structure stsT := Sts {
......
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