Commit 453a3791 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix implicit arguments of gset CMRA.

parent 6e10b9aa
...@@ -84,3 +84,6 @@ Section gset. ...@@ -84,3 +84,6 @@ Section gset.
rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver. rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver.
Qed. Qed.
End gset. End gset.
Arguments gset_disjR _ {_ _}.
Arguments gset_disjUR _ {_ _}.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment