@psteckler One of the things I'm used to do for really long-running developments is to ask Coq to "type check until point", but then to maximize the window and keep editing after point. It could take Coq several minutes to reach the point I had requested, and so I can get work done during that time.
With the async branch, Coq insists on having the Goals window displayed, which takes up half the frame. If I use C-x 1 to make it go away so I can keep editing, PG will branch it right back a few seconds later.
This makes it much harder to edit code while existing code is being type checked.
@psteckler One of the things I'm used to do for really long-running developments is to ask Coq to "type check until point", but then to maximize the window and keep editing after point. It could take Coq several minutes to reach the point I had requested, and so I can get work done during that time.
With the async branch, Coq insists on having the Goals window displayed, which takes up half the frame. If I use
C-x 1to make it go away so I can keep editing, PG will branch it right back a few seconds later.This makes it much harder to edit code while existing code is being type checked.