From 453a3791e56d12d0937b29532fcd98b744d9fe23 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Mon, 25 Jul 2016 16:21:12 +0200 Subject: [PATCH] Fix implicit arguments of gset CMRA. --- algebra/gset.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/algebra/gset.v b/algebra/gset.v index cca312c3a..10eefcfc9 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 _ {_ _}. -- GitLab