From d1d44e55f630633ba99c314b4c26f344d7d0ab12 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 14 Feb 2021 17:26:21 -0500
Subject: [PATCH] Small patch for Coq 8.13

---
 ConcurrentSeparationLogic.v          | 4 ++--
 ConcurrentSeparationLogic_template.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v
index 0f23113..2c02807 100644
--- a/ConcurrentSeparationLogic.v
+++ b/ConcurrentSeparationLogic.v
@@ -698,7 +698,7 @@ Proof.
   simp.
   rewrite Heq in H0.
   simp.
-  equality.
+  try equality.
   cancel.
   cancel.
   cancel.
@@ -823,7 +823,7 @@ Proof.
   simp.
   rewrite Heq in H0.
   simp.
-  equality.
+  try equality.
   cancel.
   cancel.
   cancel.
diff --git a/ConcurrentSeparationLogic_template.v b/ConcurrentSeparationLogic_template.v
index 96acab4..3f9d7cb 100644
--- a/ConcurrentSeparationLogic_template.v
+++ b/ConcurrentSeparationLogic_template.v
@@ -743,7 +743,7 @@ Proof.
   simp.
   rewrite Heq in H0.
   simp.
-  equality.
+  try equality.
   cancel.
   cancel.
   cancel.