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.