From 34918ec983f52f523ea520e0cc02e98ba62da1ca Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Tue, 8 Aug 2023 17:10:13 +0200
Subject: [PATCH] Fix missing ucmra_unit, ucmra_ofeO
---
iris/algebra/cmra.v | 15 ++++++++++-----
1 file changed, 10 insertions(+), 5 deletions(-)
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 153e111b3..1cf192616 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -113,7 +113,9 @@ Canonical Structure cmra_ofeO.
For these structures, we instruct Coq to eagerly _expand_ all projections,
except for the coercion to type (in this case, [cmra_car]), since that causes
- problem with canonical structure inference. *)
+ problem with canonical structure inference. Additionally, we make Coq
+ eagerly expand the coercions that go from one structure to another, like
+ [cmra_ofeO] in this case. *)
Global Strategy expand [cmra_ofeO cmra_equiv cmra_dist cmra_pcore cmra_op
cmra_valid cmra_validN cmra_ofe_mixin cmra_mixin].
@@ -246,13 +248,16 @@ Canonical Structure ucmra_cmraR.
(* As explained more thoroughly in iris#539, Coq can run into trouble when
[cmra] combinators (such as [optionUR]) are stacked and combined with
coercions like [ucmra_cmraR]. To partially address this, we give Coq's
- type-checker some directions for unfolding, with the Strategy command.
+ type-checker some directions for unfolding, with the command.
For these structures, we instruct Coq to eagerly _expand_ all projections,
except for the coercion to type (in this case, [ucmra_car]), since that causes
- problem with canonical structure inference. *)
-Global Strategy expand [ucmra_cmraR ucmra_equiv ucmra_dist ucmra_pcore ucmra_op
- ucmra_valid ucmra_validN ucmra_ofe_mixin ucmra_cmra_mixin].
+ problem with canonical structure inference. Additionally, we make Coq
+ eagerly expand the coercions that go from one structure to another, like
+ [ucmra_cmraR] and [ucmra_ofeO] in this case. *) *)
+Global Strategy expand [ucmra_cmraR ucmra_ofeO ucmra_equiv ucmra_dist ucmra_pcore
+ ucmra_op ucmra_valid ucmra_validN ucmra_unit
+ ucmra_ofe_mixin ucmra_cmra_mixin].
(** Lifting properties from the mixin *)
Section ucmra_mixin.
--
GitLab