Merge pull request #144 from uwplse/conclude_using

simplified conclude_using
uwplse · Nov 5, 2023 · f082f86 · f082f86
2 parents 44aacdc + 0f15fa5
commit f082f86
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.