Alternative definition of the basic update modality (!211) · Merge requests · Iris / Iris · GitLab

Merged Robbert Krebbers requested to merge robbert/bupd_alt into master Jan 26, 2019

This MR replaces the "double negation" file with the alternative definition of basic updates from https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/186.