Stream: Coq users

Topic: ✔ Bug in Tactician

view this post on Zulip Notification Bot (Apr 10 2024 at 14:05):

Huỳnh Trần Khanh has marked this topic as resolved.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 10 2024 at 14:27):

There is an option to make the cursor behavior different; this has been a tricky point, depending how people work they may want the goals be shown in different ways.

view this post on Zulip Théo Winterhalter (Apr 10 2024 at 14:29):

I'm too used to manual mode to put my cursor anywhere else. :smile:

view this post on Zulip Ali Caglayan (Apr 10 2024 at 16:00):

Oh that explains why I didn't see an issue. Because I use coq-lsp all the time. :laughing:

Last updated: Jun 13 2024 at 19:02 UTC