Skip to content

Remove an unused argument for `newcounter_mono_spec`.

Dan Frumin requested to merge dfrumin/iris-coq:quickfix into master

The monotonic counter does not really assert ownership of any propositions, so R : iProp \Sigma is just a dangling argument to newcounter_mono_spec.

Merge request reports