Skip to content
GitLab

Add option_local_update_None

Merged Ralf Jung requested to merge ralf/option-local-update into master

This is the (hopefully) uncontroversial part of !371 (closed). Lemma and proof by Dmitry Khalanskiy.