Skip to content

Tweak lemmas for discrete and total `cmra_update`

Robbert Krebbers requested to merge robbert/cmra_update_discrete into master

The existing lemmas cmra_discrete_update and cmra_discrete_updateP required both CmraDiscrete and CmraTotal.

This MR renames cmra_discrete_update → cmra_discrete_total_update and cmra_discrete_updateP → cmra_discrete_total_updateP. It uses the existing lemmas for versions with only CmraDiscrete.

Merge request reports