Commit 1d628d4b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Do not let simple unfold structure projections.

parent f4bb2c39
......@@ -52,6 +52,17 @@ Structure cmraT := CMRAT {
cmra_extend : CMRAExtend cmra_car
}.
Arguments CMRAT _ {_ _ _ _ _ _ _ _ _ _ _}.
Arguments cmra_car _ : simpl never.
Arguments cmra_equiv _ _ _ : simpl never.
Arguments cmra_dist _ _ _ _ : simpl never.
Arguments cmra_compl _ _ : simpl never.
Arguments cmra_unit _ _ : simpl never.
Arguments cmra_op _ _ _ : simpl never.
Arguments cmra_valid _ _ : simpl never.
Arguments cmra_validN _ _ _ : simpl never.
Arguments cmra_included _ _ _ : simpl never.
Arguments cmra_minus _ _ _ : simpl never.
Arguments cmra_cmra _ : simpl never.
Add Printing Constructor cmraT.
Existing Instances cmra_equiv cmra_dist cmra_compl cmra_unit cmra_op
cmra_valid cmra_validN cmra_included cmra_minus cmra_cmra cmra_extend.
......
......@@ -138,7 +138,7 @@ Section map.
* by intros m1 m2 Hm i; rewrite !lookup_fmap; apply included_preserving.
* by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
Qed.
Local Hint Extern 0 => simpl; apply map_fmap_ne : typeclass_instances.
Hint Resolve (map_fmap_ne (M:=M)) : typeclass_instances.
Definition mapRA_map {A B : cmraT} (f : A -n> B) : mapRA A -n> mapRA B :=
CofeMor (fmap f : mapRA A mapRA B).
Global Instance mapRA_map_ne {A B} n :
......
......@@ -45,6 +45,11 @@ Structure cofeT := CofeT {
Arguments CofeT _ {_ _ _ _}.
Add Printing Constructor cofeT.
Existing Instances cofe_equiv cofe_dist cofe_compl cofe_cofe.
Arguments cofe_car _ : simpl never.
Arguments cofe_equiv _ _ _ : simpl never.
Arguments cofe_dist _ _ _ _ : simpl never.
Arguments cofe_compl _ _ : simpl never.
Arguments cofe_cofe _ : simpl never.
(** General properties *)
Section cofe.
......
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