From 1d628d4bc6ce7514d82914038921b55d627b040a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 19 Nov 2015 09:31:40 +0100
Subject: [PATCH] Do not let simple unfold structure projections.
---
iris/cmra.v | 11 +++++++++++
iris/cmra_maps.v | 2 +-
iris/cofe.v | 5 +++++
3 files changed, 17 insertions(+), 1 deletion(-)
diff --git a/iris/cmra.v b/iris/cmra.v
index d94b0b1fb..e4c5589ae 100644
--- a/iris/cmra.v
+++ b/iris/cmra.v
@@ -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.
diff --git a/iris/cmra_maps.v b/iris/cmra_maps.v
index 467f3951b..68591bece 100644
--- a/iris/cmra_maps.v
+++ b/iris/cmra_maps.v
@@ -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 :
diff --git a/iris/cofe.v b/iris/cofe.v
index 38fc2051a..eb43c721c 100644
--- a/iris/cofe.v
+++ b/iris/cofe.v
@@ -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.
--
GitLab