Gah. Try again.

GaloisInc · Oct 16, 2024 · 5b6b794 · 5b6b794
1 parent 418d265
commit 5b6b794
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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 with coq-paco 4.1.2 *)
+        (* 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.