From 1f3636b0131aa1fa360f3b5e78c376724964a65c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Jun 2016 17:27:37 +0200
Subject: [PATCH] Define projections of cofeT, cmraT and ucmraT as Hint Extern.
This way, we can use eapply instead of class_apply, which is used
when the instances are defined using the Instance command. It seems
that eapply is stronger as class_apply, and as such solves some issues
when canonical structures have type class parameters, for example:
Goal Op (option (dec_agree nat)). apply _.
This failed, but is fixed by this commit.
---
algebra/cmra.v | 7 +++++--
algebra/cofe.v | 4 +++-
2 files changed, 8 insertions(+), 3 deletions(-)
diff --git a/algebra/cmra.v b/algebra/cmra.v
index e01c27716..167f75c5e 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -76,7 +76,10 @@ Arguments cmra_validN : simpl never.
Arguments cmra_cofe_mixin : simpl never.
Arguments cmra_mixin : simpl never.
Add Printing Constructor cmraT.
-Existing Instances cmra_pcore cmra_op cmra_valid cmra_validN.
+Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
+Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
+Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
+Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A (cmra_cofe_mixin A).
Canonical Structure cmra_cofeC.
@@ -174,7 +177,7 @@ Arguments ucmra_cofe_mixin : simpl never.
Arguments ucmra_cmra_mixin : simpl never.
Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmraT.
-Existing Instances ucmra_empty.
+Hint Extern 0 (Empty _) => eapply (@ucmra_empty _) : typeclass_instances.
Coercion ucmra_cofeC (A : ucmraT) : cofeT := CofeT A (ucmra_cofe_mixin A).
Canonical Structure ucmra_cofeC.
Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
diff --git a/algebra/cofe.v b/algebra/cofe.v
index dcfaa6355..f628b2fe9 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -67,7 +67,9 @@ Structure cofeT := CofeT {
}.
Arguments CofeT _ {_ _ _} _.
Add Printing Constructor cofeT.
-Existing Instances cofe_equiv cofe_dist cofe_compl.
+Hint Extern 0 (Equiv _) => eapply (@cofe_equiv _) : typeclass_instances.
+Hint Extern 0 (Dist _) => eapply (@cofe_dist _) : typeclass_instances.
+Hint Extern 0 (Compl _) => eapply (@cofe_compl _) : typeclass_instances.
Arguments cofe_car : simpl never.
Arguments cofe_equiv : simpl never.
Arguments cofe_dist : simpl never.
--
GitLab