From 3fd5ba7353467d26aa88f89bb6baf9ec13387a23 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Tue, 8 Aug 2023 17:10:50 +0200
Subject: [PATCH] No longer doubly closing comment
---
iris/algebra/cmra.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 1cf192616..050079f69 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -254,7 +254,7 @@ Canonical Structure ucmra_cmraR.
except for the coercion to type (in this case, [ucmra_car]), since that causes
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. *) *)
+ [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].
--
GitLab