Merge branch 'ralf/mono_nat_update' into 'master'

mono_nat_update: make first argument implicit See merge request iris/iris!600

Merge branch 'ralf/mono_nat_update' into 'master'
mono_nat_update: make first argument implicit See merge request iris/iris!600
37b991f3 · Ralf Jung · e23bc97f · 93c00401 · 37b991f3
Commit 37b991f3 authored 4 years ago by Ralf Jung
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -79,7 +79,7 @@ Section mono_nat.
  Lemma mono_nat_included q n : mono_nat_lb n ≼ mono_nat_auth q n.
  Proof. apply cmra_included_r. Qed.

-  Lemma mono_nat_update n n' :
+  Lemma mono_nat_update {n} n' :
    n ≤ n' →
    mono_nat_auth 1 n ~~> mono_nat_auth 1 n'.
  Proof.