diff --git a/algebra/gset.v b/algebra/gset.v index cca312c3a475b5260037f1a87e24523d5b2cdb37..10eefcfc936939d519dfcb4a229c39e4ef5328c4 100644 --- a/algebra/gset.v +++ b/algebra/gset.v @@ -84,3 +84,6 @@ Section gset. rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver. Qed. End gset. + +Arguments gset_disjR _ {_ _}. +Arguments gset_disjUR _ {_ _}.