Commit 1f3636b0 authored by Robbert Krebbers's avatar Robbert Krebbers

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.
parent 35bba4ed
Pipeline #1420 passed with stage
......@@ -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 :=
......
......@@ -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.
......
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