Skip to content
Snippets Groups Projects
Commit a7b31dd6 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix proof for Coq 8.20

parent df78e928
No related branches found
No related tags found
No related merge requests found
Pipeline #110014 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/logic/satisfiable.v
+ 1
− 1
View file @ a7b31dd6
......@@ -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.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment