simplified conclude_using

uwplse · Nov 5, 2023 · 0f15fa5 · 0f15fa5
1 parent 44aacdc
commit 0f15fa5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.