From 75f40fe081bbb32b9f57577596687d631f9520b0 Mon Sep 17 00:00:00 2001
From: David Holland <dholland@galois.com>
Date: Wed, 16 Oct 2024 17:15:23 -0400
Subject: [PATCH] Require coq-paco >= 4.2.1 rather than 4.1.2.

The change from 4.2.0 to 4.2.1 was what caused the previous build
breakage.

Also update the comment about it to reflect this.
---
 opam                           | 2 +-
 theories/Ref/EnTreeSpecFacts.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/opam b/opam
index 4962a22..fec93b8 100644
--- a/opam
+++ b/opam
@@ -12,7 +12,7 @@ depends: [
   "ocamlfind"
   "coq" {>= "8.15" & < "8.16"}
   "coq-itree" {>= "5.2" & < "5.3"}
-  "coq-paco" {>= "4.1.2"}
+  "coq-paco" {>= "4.2.1"}
 ]
 build: [
   [make]
diff --git a/theories/Ref/EnTreeSpecFacts.v b/theories/Ref/EnTreeSpecFacts.v
index b9a1170..3616824 100644
--- a/theories/Ref/EnTreeSpecFacts.v
+++ b/theories/Ref/EnTreeSpecFacts.v
@@ -431,7 +431,7 @@ Proof.
       * constructor; auto. intros. eapply H0 in H2. right. pclearbot.
         eapply CIH; eauto with solve_padded.
         2 : apply REL.
-        (* these bits no longer needed 20241014 *)
+        (* these bits no longer needed with coq-paco 4.2.1 *)
         (* 2 : destruct H2; try contradiction; auto. *)
         inv Hpad1. inj_existT. subst. pstep.
         constructor. auto.