Romain Tetley
Romain Tetley
WIP for making faster and better highlights Closes #743 Closes #657 Closes #642
Currently, the parser does not handle comments. This causes havoc in many cases: - When large files have a lot of comments this causes performance issues - When lines are...
The following example creates a weird bug. To reproduce step forward and backward on top of the document. This will issue a warning. ``` Require Import Extraction. Module plus. End...
This issue was reported on zulip here: https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs-.26-users/topic/Cannot.20add.20monomorphic.20constraints/near/408931549
Loosely related to #537 When performing a query while in error state (right after having executed a line with an error), queries do not work. Searches return no results and...
As specified in #344 we actually need a third mode -> electric terminator (i.e. each time a correct sentence is written by the user we perform a stepForward).
Write an optimizer for the event loop. This module will pre-process the event list to make sure everything is done optimally. One such feature: check that there is only ONE...
Sometimes the search queries yield lots of results. It would be a nice feature to be able to interrupt an ongoing Search.
On my setup, trying to install conf-ppl results on the following error: ``` [ERROR] The compilation of conf-ppl.1 failed at "sh -c cc test.c -lppl_c -lppl". #=== ERROR while compiling...
This issue exists to track the issues on the package upstream repos to create tags for Coq 8.19. This ticket is referenced in all package issues. Discussions should take place...