From a7b31dd67982dbe35acdd03294e5095ec5880b3f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 2 Oct 2024 17:00:02 +0200
Subject: [PATCH] fix proof for Coq 8.20
---
theories/logic/satisfiable.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/logic/satisfiable.v b/theories/logic/satisfiable.v
index 7ea61a8f..4ca6546c 100644
--- a/theories/logic/satisfiable.v
+++ b/theories/logic/satisfiable.v
@@ -30,7 +30,7 @@ Section satisfiable.
Global Instance sat_equiv: Proper ((≡) ==> iff) sat.
Proof.
- intros P Q Heq; split; intros Hsat; eauto using sat_mono, equiv_entails_1_1, equiv_entails_1_2.
+ intros P Q Heq; split; intros Hsat; (eapply sat_mono; last done); eauto using equiv_entails_1_1, equiv_entails_1_2.
Qed.
Lemma sat_sep P Q: sat (P ∗ Q) → sat P ∧ sat Q.
--
GitLab