This also gets rid of [val_for_compare]-normalization; instead we introduce a
[LitErased] literal that is suited for use by erasure theorems.

This commit made me cry...

Created this commit with pain in my heart!

show auth_update_core_id

See merge request iris!282

Prove sigT_equivI is admissible (fix #250)

Closes #250

See merge request iris!280

One of the new proofs needs `sigTO`, so move others together.

Fix typos in comments

See merge request iris!281

Turn CAS from compare-and-set to compare-and-swap

See merge request iris!274

This is the name used by x86 (CMPXCHG) and LLVM.  Also reorder the result (value
first, boolean second) for consistency with LLVM, because why not.

Cofe and cFunctor for sigT

See merge request iris!278

Fix sed on mac for real

See merge request iris!277

Paolo G. Giarrusso authored Jun 21, 2019 and Ralf Jung committed Jun 21, 2019

On Mac, options must come first. On Linux this should still be fine, and works
with gnu-sed.