From 0f15fa54ee04999d6fdabb9a807a3c0ad5d53980 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 5 Nov 2023 08:46:03 +0100 Subject: [PATCH] simplified conclude_using --- theories/Systems/LiveLockServ.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Systems/LiveLockServ.v b/theories/Systems/LiveLockServ.v index a4bf5d93..899d782c 100644 --- a/theories/Systems/LiveLockServ.v +++ b/theories/Systems/LiveLockServ.v @@ -2111,7 +2111,7 @@ Section LockServ. intros. pose proof (@clients_move_way_up_in_queue n 0 c s). pose proof (Nat.le_0_l n). - repeat concludes. conclude_using ltac:(intuition; congruence). + repeat concludes. conclude_using (intuition; congruence). eapply eventually_monotonic_simple; [|eauto]. intros. simpl in *. intuition. Qed.