diff --git a/iris/algebra/coPset.v b/iris/algebra/coPset.v index 7a987611969ff5c97ec822e6505304d4e6018af7..aba562c4299d79cca7e497d2139982c0d1870456 100644 --- a/iris/algebra/coPset.v +++ b/iris/algebra/coPset.v @@ -60,7 +60,7 @@ Section coPset. Qed. End coPset. -(* The disjoiny union CMRA *) +(* The disjoint union CMRA *) Inductive coPset_disj := | CoPset : coPset → coPset_disj | CoPsetBot : coPset_disj.