From b3e550a1bd77c73d49c20ef0dcc4f161efd08dc4 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 5 Mar 2020 23:16:27 +0100 Subject: [PATCH] Coq 8.10 compat. --- theories/sets.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/sets.v b/theories/sets.v index 02f52822..c6bdf3e4 100644 --- a/theories/sets.v +++ b/theories/sets.v @@ -1032,9 +1032,9 @@ Section pred_finite_infinite. Qed. Lemma pred_finite_le n : pred_finite (flip le n). - Proof. eapply pred_finite_impl; [apply (pred_finite_lt (S n))|]; simpl; lia. Qed. + Proof. eapply pred_finite_impl; [apply (pred_finite_lt (S n))|]; naive_solver lia. Qed. Lemma pred_infinite_le n : pred_infinite (le n). - Proof. eapply pred_infinite_impl; [apply (pred_infinite_lt (S n))|]; simpl; lia. Qed. + Proof. eapply pred_infinite_impl; [apply (pred_infinite_lt (S n))|]; naive_solver lia. Qed. End pred_finite_infinite. Section set_finite_infinite. -- GitLab