From 8fc19c9d104976494ae3ed419c98578dfef5d464 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 15 Feb 2023 15:49:39 +0100
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/16788

---
 iris_heap_lang/primitive_laws.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 69948ca6e..6373e48be 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -207,10 +207,10 @@ Proof. apply mapsto_valid. Qed.
 Lemma mapsto_valid_2 l dq1 dq2 v1 v2 :
   l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
 Proof.
-  iIntros "H1 H2". iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=?]]. done.
+  iIntros "H1 H2". iDestruct (mapsto_valid_2 with "H1 H2") as %[? [= ?]]. done.
 Qed.
 Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
-Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=?]. done. Qed.
+Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[= ?]. done. Qed.
 
 Lemma mapsto_combine l dq1 dq2 v1 v2 :
   l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
-- 
GitLab