Will Thomas

What would your thoughts be on a possible alternate approach where we basically have two phases of minification: 1. Directly import all transitively depended upon files 2. Work forward (i.e....

A workaround is demonstrated in the GIF as well showing that if you have a `*.v` or `_CoqProject` file focused, then swap to the Search sidebar (could be any other),...

It produces the following for me using 'JetBrainsMono Nerd Font Mono' and the underscores are present:  I also tested with Consolas, 'Courier New', and monospace and they all seem...

I installed Fira Code and tried it in VsCode v1.93.0 (on Windows via WSL) and got this:  Are you using vscodium and/or not windows? Might be related to one...

I have been able to reproduce this with `monospace` on Linux and vscode, but the exact same setup on Windows with font `monospace` does not cause the issue.

I think I have tracked down the offending font: `DejaVu Sans Mono` I can confirm that with this font the underscores are not displayed in Linux, but even with `DejaVu...

I was looking around at the proposed solution to display an unformatted goal first and found the following results: **Formatted**  **Unformatted**  My timing/synchronization was not very precise, but...

Good catch on the makefile @gares, should be fixed now. Also pushed some documentation and an initial test case to hopefully make the goal of this PR more clear.

> Do we need yet another option? Would not it be sufficient to teach `coq_makefile` that, if it finds a `_CoqProject` file at the target directory of a `-R` or...

So it seems that my initial crack at this still has design issues to be worked out. I will look into a new solution that hopefully addresses all the concerns....