Skip to content

Alternative definition of the basic update modality

Robbert Krebbers requested to merge robbert/bupd_alt into master

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.

Merge request reports