From 038f8e0e220d944bf396b564378e316c82a46f8c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 7 Jan 2017 10:25:32 +0100
Subject: [PATCH] Make instances EqDecision and Countable of gmultiset less
eager.
Fix fixes issue #63.
---
theories/prelude/gmultiset.v | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/theories/prelude/gmultiset.v b/theories/prelude/gmultiset.v
index 0cda0e1c4..fefe1aed4 100644
--- a/theories/prelude/gmultiset.v
+++ b/theories/prelude/gmultiset.v
@@ -7,14 +7,18 @@ Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
Arguments GMultiSet {_ _ _} _.
Arguments gmultiset_car {_ _ _} _.
-Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
+Lemma gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
Proof. solve_decision. Defined.
+Hint Extern 1 (Decision (@eq (gmultiset _) _ _)) =>
+ eapply @gmultiset_eq_dec : typeclass_instances.
-Program Instance gmultiset_countable `{Countable A} :
+Program Definition gmultiset_countable `{Countable A} :
Countable (gmultiset A) := {|
encode X := encode (gmultiset_car X); decode p := GMultiSet <$> decode p
|}.
Next Obligation. intros A ?? [X]; simpl. by rewrite decode_encode. Qed.
+Hint Extern 1 (Countable (gmultiset _)) =>
+ eapply @gmultiset_countable : typeclass_instances.
Section definitions.
Context `{Countable A}.
--
GitLab