From bf069d128966a74d73b180a7b0ddaee6d781210c Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 31 Jan 2017 09:26:26 +0100 Subject: [PATCH] Arguments for gsetC and gset_disjC. --- theories/algebra/gset.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v index 7b1756919..5fb4622c5 100644 --- a/theories/algebra/gset.v +++ b/theories/algebra/gset.v @@ -59,6 +59,7 @@ Section gset. Proof. by apply persistent_total; rewrite gset_core_self. Qed. End gset. +Arguments gsetC _ {_ _}. Arguments gsetR _ {_ _}. Arguments gsetUR _ {_ _}. @@ -220,5 +221,6 @@ Section gset_disj. Qed. End gset_disj. +Arguments gset_disjC _ {_ _}. Arguments gset_disjR _ {_ _}. Arguments gset_disjUR _ {_ _}. -- GitLab